From 17c08a2309efd91f8c4f5a9c761bf6d8ac4e4d01 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Wed, 24 Sep 2025 22:38:28 -0600 Subject: [PATCH 1/6] organize Utxo.Properties and Certs.Properties and fix resulting issues in Ledger.Properties --- build-tools/static/md/nav.yml | 2 + .../Specification/Certs/Properties.agda | 152 ----- .../Certs/Properties/PoV.lagda.md | 6 +- .../Certs/Properties/PoVLemmas.lagda.md | 2 +- .../Ledger/Properties/PoV.lagda.md | 13 +- .../Specification/Utxo/Properties.lagda | 575 +----------------- .../Utxo/Properties/DepositHelpers.agda | 422 +++++++++++++ .../Utxo/Properties/GenMinSpend.lagda.md | 192 ++++++ .../Utxo/Properties/MinSpend.lagda.md | 108 +--- .../Utxo/Properties/PoV.lagda.md | 6 +- 10 files changed, 652 insertions(+), 826 deletions(-) create mode 100644 src/Ledger/Conway/Specification/Utxo/Properties/DepositHelpers.agda create mode 100644 src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md diff --git a/build-tools/static/md/nav.yml b/build-tools/static/md/nav.yml index 4c4b901d7..d4c219412 100644 --- a/build-tools/static/md/nav.yml +++ b/build-tools/static/md/nav.yml @@ -96,6 +96,8 @@ - Utxo/: - Properties: Ledger.Conway.Specification.Utxo.Properties.md - Properties/: + - DepositHelpers: Ledger.Conway.Specification.Utxo.Properties.DepositHelpers.md + - GenMinspend: Ledger.Conway.Specification.Utxo.Properties.GenMinSpend.md - MinSpend: Ledger.Conway.Specification.Utxo.Properties.MinSpend.md - PoV: Ledger.Conway.Specification.Utxo.Properties.PoV.md - Utxow: Ledger.Conway.Specification.Utxow.md diff --git a/src/Ledger/Conway/Specification/Certs/Properties.agda b/src/Ledger/Conway/Specification/Certs/Properties.agda index 752758649..0bfa66a5c 100644 --- a/src/Ledger/Conway/Specification/Certs/Properties.agda +++ b/src/Ledger/Conway/Specification/Certs/Properties.agda @@ -161,155 +161,3 @@ instance Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String Computational-CERTS = it - -private variable - dCert : DCert - l : List DCert - A A' B : Type -instance - _ = +-0-monoid - -getCoin-singleton : ⦃ _ : DecEq A ⦄ {(a , c) : A × Coin} → indexedSumᵛ' id ❴ (a , c) ❵ ≡ c -getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _) - -∪ˡsingleton∈dom : ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin} - → a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m -∪ˡsingleton∈dom m {(a , c)} a∈dom = ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵) m (singleton-∈-∪ˡ {m = m} a∈dom) - -module _ {Γ : CertEnv} - ( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → disjoint (dom m) (dom m') - → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' ) - where - open ≡-Reasoning - open Equivalence - - ∪ˡsingleton∉dom : ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin} - → a ∉ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m + c - ∪ˡsingleton∉dom m {(a , c)} a∉dom = begin - getCoin (m ∪ˡ ❴ a , c ❵ᵐ) - ≡⟨ indexedSumᵛ'-∪ m ❴ a , c ❵ᵐ - ( λ x y → a∉dom (subst (_∈ dom m) (from ∈-dom-singleton-pair y) x) ) ⟩ - getCoin m + getCoin ❴ a , c ❵ᵐ - ≡⟨ cong (getCoin m +_) getCoin-singleton ⟩ - getCoin m + c - ∎ - - ∪ˡsingleton0≡ : ⦃ _ : DecEq A ⦄ → (m : A ⇀ Coin) {a : A} → getCoin (m ∪ˡ ❴ (a , 0) ❵ᵐ) ≡ getCoin m - ∪ˡsingleton0≡ m {a} with a ∈? dom m - ... | yes a∈dom = ∪ˡsingleton∈dom m a∈dom - ... | no a∉dom = trans (∪ˡsingleton∉dom m a∉dom) (+-identityʳ (getCoin m)) - - - CERT-pov : {stᵈ stᵈ' : DState} {stᵖ stᵖ' : PState} {stᵍ stᵍ' : GState} - → Γ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ - → getCoin ⟦ stᵈ , stᵖ , stᵍ ⟧ ≡ getCoin ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ - CERT-pov (CERT-deleg (DELEG-delegate {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds) - CERT-pov (CERT-deleg (DELEG-reg {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds) - CERT-pov {stᵖ = stᵖ} {stᵖ'} {stᵍ} {stᵍ'} - (CERT-deleg (DELEG-dereg {c = c} {rwds} {vDelegs = vDelegs}{sDelegs} x)) = begin - getCoin ⟦ ⟦ vDelegs , sDelegs , rwds ⟧ , stᵖ , stᵍ ⟧ - ≡˘⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp rwds - ( ≡ᵉ.trans rwds-∪ˡ-∪ (≡ᵉ.trans ∪-sym (res-ex-∪ Dec-∈-singleton)) ) ⟩ - getCoin rwds-∪ˡ-decomp - ≡⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ) rwds-∪ˡ≡sing-∪ˡ ⟩ - getCoin ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ ) - ≡⟨ ∪ˡsingleton0≡ (rwds ∣ ❴ c ❵ ᶜ) ⟩ - getCoin ⟦ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ , stᵖ' , stᵍ' ⟧ - ∎ - where - module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin}) - rwds-∪ˡ-decomp = (rwds ∣ ❴ c ❵ ᶜ) ∪ˡ (rwds ∣ ❴ c ❵ ) - - rwds-∪ˡ-∪ : rwds-∪ˡ-decomp ˢ ≡ᵉ (rwds ∣ ❴ c ❵ ᶜ)ˢ ∪ (rwds ∣ ❴ c ❵)ˢ - rwds-∪ˡ-∪ = disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint) - - disj : disjoint (dom ((rwds ∣ ❴ c ❵ˢ ᶜ) ˢ)) (dom (❴ c , 0 ❵ᵐ ˢ)) - disj {a} a∈res a∈dom = res-comp-dom a∈res (dom-single→single a∈dom) - - rwds-∪ˡ≡sing-∪ˡ : rwds-∪ˡ-decomp ˢ ≡ᵉ ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )ˢ - rwds-∪ˡ≡sing-∪ˡ = ≡ᵉ.trans rwds-∪ˡ-∪ - ( ≡ᵉ.trans (∪-cong ≡ᵉ.refl (res-singleton'{m = rwds} x)) - (≡ᵉ.sym $ disjoint-∪ˡ-∪ disj) ) - CERT-pov (CERT-pool x) = refl - CERT-pov (CERT-vdel x) = refl - - injOn : (wdls : Withdrawals) - → ∀[ a ∈ dom (wdls ˢ) ] NetworkIdOf a ≡ NetworkId - → InjectiveOn (dom (wdls ˢ)) RwdAddr.stake - injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl = - cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈))) - - module CERTSpov - -- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`. - ( sumConstZero : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 ) - ( res-decomp : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ ) - ( getCoin-cong : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s' - → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' ) - ( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'} - → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) - ( constNetworkId : ∀[ a ∈ dom (CertEnv.wdrls Γ) ] NetworkIdOf a ≡ NetworkId ) - where - - CERTBASE-pov : {s s' : CertState} → Γ ⊢ s ⇀⦇ _ ,CERTBASE⦈ s' - → getCoin s ≡ getCoin s' + getCoin (CertEnv.wdrls Γ) - - CERTBASE-pov {s = cs} - {s' = cs'} - (CERT-base {pp}{vs}{e}{dreps}{wdrls} (_ , wdrlsCC⊆rwds)) = - let - open DState (dState cs ) - open DState (dState cs') renaming (rewards to rewards') - module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin}) - wdrlsCC = mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) - zeroMap = constMap (mapˢ RwdAddr.stake (dom wdrls)) 0 - rwds-∪ˡ-decomp = (rewards ∣ dom wdrlsCC ᶜ) ∪ˡ (rewards ∣ dom wdrlsCC) - in - begin - getCoin rewards - ≡˘⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp rewards - ( ≡ᵉ.trans (disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint)) - (≡ᵉ.trans ∪-sym (res-ex-∪ (_∈? dom wdrlsCC))) ) ⟩ - getCoin rwds-∪ˡ-decomp - ≡⟨ indexedSumᵛ'-∪ (rewards ∣ dom wdrlsCC ᶜ) (rewards ∣ dom wdrlsCC) - (disjoint-sym res-ex-disjoint) ⟩ - getCoin (rewards ∣ dom wdrlsCC ᶜ) + getCoin (rewards ∣ dom wdrlsCC ) - ≡⟨ cong (getCoin (rewards ∣ dom wdrlsCC ᶜ) +_) - ( getCoin-cong (rewards ∣ dom wdrlsCC) wdrlsCC (res-subset{m = rewards} wdrlsCC⊆rwds) ) ⟩ - getCoin (rewards ∣ dom wdrlsCC ᶜ) + getCoin wdrlsCC - ≡⟨ cong (getCoin (rewards ∣ dom wdrlsCC ᶜ) +_) (≡ᵉ-getCoinˢ (wdrls ˢ) (injOn wdrls constNetworkId)) ⟩ - getCoin (rewards ∣ dom wdrlsCC ᶜ) + getCoin wdrls - ≡˘⟨ cong (_+ getCoin wdrls) - ( begin - getCoin (zeroMap ∪ˡ rewards) - ≡⟨ ≡ᵉ-getCoin (zeroMap ∪ˡ rewards) (zeroMap ∪ˡ (rewards ∣ dom zeroMap ᶜ)) - (res-decomp zeroMap rewards) ⟩ - getCoin (zeroMap ∪ˡ (rewards ∣ dom zeroMap ᶜ)) - ≡⟨ indexedSumᵛ'-∪ zeroMap (rewards ∣ dom zeroMap ᶜ) - (disjoint-sym res-comp-dom) ⟩ - getCoin zeroMap + getCoin (rewards ∣ dom zeroMap ᶜ) - ≡⟨ cong (λ u → u + getCoin (rewards ∣ dom zeroMap ᶜ)) sumConstZero ⟩ - 0 + getCoin (rewards ∣ (dom zeroMap) ᶜ) - ≡⟨ +-identityˡ (getCoin (rewards ∣ dom zeroMap ᶜ)) ⟩ - getCoin (rewards ∣ dom zeroMap ᶜ) - ≡⟨ ≡ᵉ-getCoin (rewards ∣ dom zeroMap ᶜ) (rewards ∣ dom wdrlsCC ᶜ) - ( res-comp-cong - ( ⊆-Transitive (proj₁ constMap-dom) (proj₂ dom-mapˡ≡map-dom) - , ⊆-Transitive (proj₁ dom-mapˡ≡map-dom) (proj₂ constMap-dom) ) ) ⟩ - getCoin (rewards ∣ dom wdrlsCC ᶜ) - ∎ ) ⟩ - getCoin (zeroMap ∪ˡ rewards) + getCoin wdrls - ∎ - - sts-pov : {s₁ sₙ : CertState} → ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,CERT⦈_} Γ s₁ l sₙ - → getCoin s₁ ≡ getCoin sₙ - sts-pov (BS-base Id-nop) = refl - sts-pov (BS-ind x xs) = trans (CERT-pov x) (sts-pov xs) - - CERTS-pov : {s₁ sₙ : CertState} → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ → getCoin s₁ ≡ getCoin sₙ + getCoin (CertEnv.wdrls Γ) - CERTS-pov (RTC {s' = s'} {s'' = sₙ} (bsts , BS-base Id-nop)) = CERTBASE-pov bsts - CERTS-pov (RTC (bsts , BS-ind x sts)) = trans (CERTBASE-pov bsts) - (cong (_+ getCoin (CertEnv.wdrls Γ)) - (trans (CERT-pov x) (sts-pov sts))) - diff --git a/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md index 24476317b..b381ae1d6 100644 --- a/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md +++ b/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md @@ -1,4 +1,4 @@ - diff --git a/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md index 4e7d3fac8..d9b7edebd 100644 --- a/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md +++ b/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md @@ -122,7 +122,7 @@ some `dcert`{.AgdaBound} : `DCert`{.AgdaDatatype}. Then, injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl = cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈))) - module CERTSpov + module CERTS-pov-helper -- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`. ( sumConstZero : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 ) ( res-decomp : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) diff --git a/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md b/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md index a030bd959..7dd964c16 100644 --- a/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md +++ b/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md @@ -13,11 +13,11 @@ module Ledger.Conway.Specification.Ledger.Properties.PoV open import Ledger.Conway.Specification.Certs govStructure open import Ledger.Conway.Specification.Chain txs abs -open import Ledger.Conway.Specification.Certs.Properties govStructure +open import Ledger.Conway.Specification.Certs.Properties.PoVLemmas govStructure +open import Ledger.Conway.Specification.Certs.Properties.PoV govStructure open import Ledger.Conway.Specification.Ledger txs abs open import Ledger.Prelude open import Ledger.Conway.Specification.Utxo txs abs -open import Ledger.Conway.Specification.Utxo.Properties txs abs using (χ; module DepositHelpers) open import Ledger.Conway.Specification.Utxo.Properties.PoV txs abs open import Ledger.Conway.Specification.Utxow txs abs @@ -81,14 +81,15 @@ then the coin values of `s`{.AgdaBound} and `s'`{.AgdaBound} are equal, that is, open LState s' renaming (utxoSt to utxoSt'; govSt to govSt'; certState to certState') open CertState certState' open ≡-Reasoning - open CERTSpov indexedSumᵛ'-∪ sumConstZero res-decomp getCoin-cong ≡ᵉ-getCoinˢ r - zeroMap = constMap (mapˢ RwdAddr.stake (dom txWithdrawals)) 0 + open CERTSpov indexedSumᵛ'-∪ sumConstZero res-decomp getCoin-cong ≡ᵉ-getCoinˢ + zeroMap = constMap (mapˢ RwdAddr.stake (dom txWithdrawals)) 0 in + begin getCoin utxoSt + getCoin certState - ≡⟨ cong (getCoin utxoSt +_) (CERTS-pov h') ⟩ + ≡⟨ cong (getCoin utxoSt +_) (CERTS-pov r h') ⟩ getCoin utxoSt + (getCoin certState' + getCoin txWithdrawals) - ≡˘⟨ cong (λ x → getCoin utxoSt + (getCoin certState' + x )) (*-identityʳ (getCoin txWithdrawals)) ⟩ -- cong (λ u → getCoin utxoSt + (getCoin certState' + getCoin txWithdrawals * χ u)) valid ⟩ + ≡˘⟨ cong (λ x → getCoin utxoSt + (getCoin certState' + x )) (*-identityʳ (getCoin txWithdrawals)) ⟩ getCoin utxoSt + (getCoin certState' + getCoin txWithdrawals * 1) ≡˘⟨ cong (λ u → getCoin utxoSt + (getCoin certState' + getCoin txWithdrawals * χ u)) valid ⟩ getCoin utxoSt + (getCoin certState' + getCoin txWithdrawals * χ isValid) diff --git a/src/Ledger/Conway/Specification/Utxo/Properties.lagda b/src/Ledger/Conway/Specification/Utxo/Properties.lagda index bd1df487b..abb929323 100644 --- a/src/Ledger/Conway/Specification/Utxo/Properties.lagda +++ b/src/Ledger/Conway/Specification/Utxo/Properties.lagda @@ -4,41 +4,31 @@ \begin{code}[hide] {-# OPTIONS --safe #-} -open import Algebra.Morphism using (module MonoidMorphisms; IsMagmaHomomorphism) -import Data.Nat as ℕ -open import Data.Nat.Properties hiding (_≟_) -open import Data.Product using (swap) -open import Data.Sign using (Sign) -open import Data.Integer as ℤ using (ℤ) -import Data.Integer.Properties as ℤ -open import Data.String.Base renaming (_++_ to _+ˢ_) using () -open import Relation.Binary using (IsEquivalence) +open import Ledger.Conway.Specification.Abstract +open import Ledger.Conway.Specification.Transaction + +module Ledger.Conway.Specification.Utxo.Properties + (txs : _) (open TransactionStructure txs) + (abs : AbstractFunctions txs) (open AbstractFunctions abs) + where +open import Algebra.Morphism using (module MonoidMorphisms; IsMagmaHomomorphism) +open import Data.Integer as ℤ using (ℤ) open import Data.List.Relation.Unary.All using (All) -open import Data.List.Relation.Unary.Any using (Any); open Any +import Data.Nat as ℕ +open import Data.Nat.Properties hiding (_≟_) +open import Data.String.Base using () renaming (_++_ to _+ˢ_) open import Prelude; open Equivalence +open import Ledger.Prelude hiding (≤-trans; ≤-antisym; All); open Properties open import Tactic.Cong using (cong!) -open import Tactic.Defaults open import Tactic.EquationalReasoning using (module ≡-Reasoning) -open import stdlib-meta.Tactic.GenError open import stdlib-meta.Tactic.MonoidSolver.NonNormalising using (solve-macro) -open import Ledger.Prelude hiding (≤-trans; ≤-antisym; All); open Properties -open import Ledger.Conway.Specification.Abstract -open import Ledger.Conway.Specification.Transaction -open import Interface.ComputationalRelation - -module Ledger.Conway.Specification.Utxo.Properties - (txs : _) (open TransactionStructure txs) - (abs : AbstractFunctions txs) (open AbstractFunctions abs) - where - open import Ledger.Conway.Specification.Utxo txs abs open import Ledger.Conway.Specification.Script.Validation txs abs open import Ledger.Conway.Specification.Certs govStructure -open import Algebra.Definitions.RawMagma +-rawMagma using () renaming (_,_ to _,≤_) instance _ = TokenAlgebra.Value-CommutativeMonoid tokenAlgebra @@ -154,391 +144,6 @@ private variable donations donations' : Donations deposits deposits' : Deposits -open MonoidMorphisms.IsMonoidHomomorphism -private - ∙-homo-Coin = IsMagmaHomomorphism.homo (isMagmaHomomorphism coinIsMonoidHomomorphism) - -opaque - unfolding balance - balance-cong : ∣ utxo ∣ ≡ᵉ ∣ utxo' ∣ → balance utxo ≈ balance utxo' - balance-cong {utxo} {utxo'} eq = indexedSumᵐ-cong {M = Value} {x = (mapValues txOutHash utxo) ᶠᵐ} {(mapValues txOutHash utxo') ᶠᵐ} (map-≡ᵉ eq) - - balance-cong-coin : ∣ utxo ∣ ≡ᵉ ∣ utxo' ∣ → cbalance utxo ≡ cbalance utxo' - balance-cong-coin {utxo} {utxo'} x = - coinIsMonoidHomomorphism .⟦⟧-cong (balance-cong {utxo} {utxo'} x) - where open MonoidMorphisms.IsMonoidHomomorphism - - balance-∪ : disjoint (dom utxo) (dom utxo') - → cbalance (utxo ∪ˡ utxo') ≡ cbalance utxo + cbalance utxo' - balance-∪ {utxo} {utxo'} h = begin - cbalance (utxo ∪ˡ utxo') - ≡⟨ ⟦⟧-cong coinIsMonoidHomomorphism - $ indexedSumᵐ-cong {f = getValueʰ ∘ proj₂} {x = (mapValues txOutHash (utxo ∪ˡ utxo')) ᶠᵐ} {((mapValues txOutHash utxo) ᶠᵐ) ∪ˡᶠ ((mapValues txOutHash utxo') ᶠᵐ)} (disjoint-∪ˡ-mapValues {M = utxo} {utxo'} _ h) - ⟩ - coin (indexedSumᵐ _ (((mapValues txOutHash utxo) ᶠᵐ) ∪ˡᶠ ((mapValues txOutHash utxo') ᶠᵐ))) - ≡⟨ ⟦⟧-cong coinIsMonoidHomomorphism - $ indexedSumᵐ-∪ {M = Value} {X = (mapValues txOutHash utxo) ᶠᵐ} {(mapValues txOutHash utxo') ᶠᵐ} - (λ x x₁ → h (dom-mapʳ⊆ x) (dom-mapʳ⊆ x₁)) - ⟩ - coin (balance utxo + balance utxo') - ≡⟨ ∙-homo-Coin _ _ ⟩ - cbalance utxo + cbalance utxo' - ∎ - where open Tactic.EquationalReasoning.≡-Reasoning {A = ℕ} (solve-macro (quoteTerm +-0-monoid)) - -module _ {txb : _} (open TxBody txb) where opaque - unfolding outs - open Tactic.EquationalReasoning.≡-Reasoning {A = ℕ} (solve-macro (quoteTerm +-0-monoid)) - - newTxid⇒disj : txId ∉ mapˢ proj₁ (dom utxo) - → disjoint' (dom utxo) (dom (outs txb)) - newTxid⇒disj id∉utxo = disjoint⇒disjoint' λ h h' → id∉utxo $ to ∈-map - (-, (case from ∈-map h' of λ where - (_ , refl , h'') → case from ∈-map h'' of λ where (_ , refl , _) → refl) , h) - - consumedCoinEquality : ∀ {pp} - → coin mint ≡ 0 - → coin (consumed pp utxoState txb) - ≡ cbalance ((UTxOState.utxo utxoState) ∣ txIns) + depositRefunds pp utxoState txb + getCoin txWithdrawals - consumedCoinEquality {utxoState} {pp} h = - let utxo = UTxOState.utxo utxoState - dRefs = depositRefunds pp utxoState txb - sWdls = getCoin txWithdrawals - in begin - coin (balance (utxo ∣ txIns) + mint + inject dRefs + inject sWdls) - ≡⟨ ∙-homo-Coin _ _ ⟩ - coin (balance (utxo ∣ txIns) + mint + inject dRefs) + coin (inject $ sWdls) - -- ≡⟨ cong (coin (balance (utxo ∣ txIns) + mint + inject dRefs) +_) (property _) ⟩ - ≡⟨ cong (coin (balance (utxo ∣ txIns) + mint + inject dRefs) +_) (coin∘inject≗id _) ⟩ - coin (balance (utxo ∣ txIns) + mint + inject dRefs) + sWdls - ≡⟨ cong (_+ sWdls) (∙-homo-Coin _ _) ⟩ - coin (balance (utxo ∣ txIns) + mint) + coin (inject $ dRefs) + sWdls --- ≡⟨ cong (λ u → coin (balance (utxo ∣ txIns) + mint) + u + sWdls) (property _) ⟩ - ≡⟨ cong (λ u → coin (balance (utxo ∣ txIns) + mint) + u + sWdls) (coin∘inject≗id _) ⟩ - coin (balance (utxo ∣ txIns) + mint) + dRefs + sWdls - ≡⟨ cong (λ u → u + dRefs + sWdls) (∙-homo-Coin _ _) ⟩ - cbalance (utxo ∣ txIns) + coin mint + dRefs + sWdls - ≡⟨ cong (λ x → cbalance (utxo ∣ txIns) + x + dRefs + sWdls) h ⟩ - cbalance (utxo ∣ txIns) + 0 + dRefs + sWdls - ≡⟨ cong (λ x → x + dRefs + sWdls) (+-identityʳ (cbalance (utxo ∣ txIns))) ⟩ - cbalance (utxo ∣ txIns) + dRefs + sWdls - ∎ - - producedCoinEquality : ∀ {pp} - → coin (produced pp utxoState txb) - ≡ cbalance (outs txb) + txFee + newDeposits pp utxoState txb + txDonation - producedCoinEquality {utxoState} {pp} = - begin - coin (balance (outs txb) + inject txFee - + inject (newDeposits pp utxoState txb) + inject txDonation) - ≡⟨ ∙-homo-Coin _ _ ⟩ - coin (balance (outs txb) + inject txFee - + inject (newDeposits pp utxoState txb)) + coin (inject txDonation) - ≡⟨ cong (_+ coin (inject txDonation)) (begin - coin (balance (outs txb) + inject txFee - + inject (newDeposits pp utxoState txb)) - ≡⟨ ∙-homo-Coin _ _ ⟩ - coin (balance (outs txb) +ᵛ inject txFee) - ℕ.+ coin (inject (newDeposits pp utxoState txb)) --- ≡⟨ cong! (property _) ⟩ - ≡⟨ cong! (coin∘inject≗id _) ⟩ - coin (balance (outs txb) +ᵛ inject txFee) - ℕ.+ newDeposits pp utxoState txb - ≡⟨ cong! (∙-homo-Coin _ _) ⟩ - coin (balance (outs txb)) ℕ.+ coin (inject txFee) - ℕ.+ newDeposits pp utxoState txb - ≡⟨ cong (λ x → cbalance (outs txb) + x + newDeposits pp utxoState txb) --- $ property txFee ⟩ - $ coin∘inject≗id txFee ⟩ - cbalance (outs txb) + txFee + newDeposits pp utxoState txb - ∎ - )⟩ - cbalance (outs txb) + txFee - + newDeposits pp utxoState txb + coin (inject txDonation) - ≡⟨ cong (cbalance (outs txb) + txFee + newDeposits pp utxoState txb +_) --- $ property _ ⟩ - $ coin∘inject≗id _ ⟩ - cbalance (outs txb) + txFee + newDeposits pp utxoState txb + txDonation - ∎ - - balValueToCoin : ∀ {pp} - → coin mint ≡ 0 - → consumed pp utxoState txb ≡ produced pp utxoState txb - → cbalance ((UTxOState.utxo utxoState) ∣ txIns) - + depositRefunds pp utxoState txb + getCoin txWithdrawals - ≡ cbalance (outs txb) + txFee + newDeposits pp utxoState txb + txDonation - balValueToCoin {utxoState} {pp} h h' = begin - cbalance ((UTxOState.utxo utxoState) ∣ txIns) + depositRefunds pp utxoState txb + getCoin txWithdrawals - ≡˘⟨ consumedCoinEquality {utxoState} {pp} h ⟩ - coin (consumed pp utxoState txb) - ≡⟨ cong! h' ⟩ - coin (produced pp utxoState txb) - ≡⟨ producedCoinEquality {utxoState} {pp} ⟩ - cbalance (outs txb) + txFee + newDeposits pp utxoState txb + txDonation - ∎ - -posPart-negPart≡x : {x : ℤ} → posPart x - negPart x ≡ x -posPart-negPart≡x {ℤ.+_ n} = refl -posPart-negPart≡x {ℤ.negsuc n} = refl - -χ : Bool → ℕ -χ false = 0 -χ true = 1 - -module DepositHelpers - {utxo utxo' : UTxO} - {fees fees' : Fees} - {deposits deposits' : Deposits} - {donations donations' : Donations} - {tx : Tx} (let open Tx tx renaming (body to txb); open TxBody txb) - {Γ : UTxOEnv} - (step : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXO⦈ - ⟦ utxo' , fees' , deposits' , donations' ⟧) - (h' : txId ∉ mapˢ proj₁ (dom utxo)) - where - open Tactic.EquationalReasoning.≡-Reasoning {A = ℕ} (solve-macro (quoteTerm +-0-monoid)) - - private - stepS : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXOS⦈ - ⟦ utxo' , fees' , deposits' , donations' ⟧ - stepS = case step of λ where - (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) → h - - pp : PParams - pp = UTxOEnv.pparams Γ - dep : Coin - dep = getCoin deposits - uDep : Coin - uDep = getCoin (updateDeposits pp txb deposits) - Δdep : ℤ - Δdep = depositsChange pp txb deposits - utxoSt : UTxOState - utxoSt = ⟦ utxo , fees , deposits , donations ⟧ - ref tot : Coin - ref = depositRefunds pp utxoSt txb - wdls = getCoin txWithdrawals - tot = newDeposits pp utxoSt txb - h : disjoint (dom (utxo ∣ txIns ᶜ)) (dom (outs txb)) - h = λ h₁ h₂ → ∉-∅ $ proj₁ (newTxid⇒disj {txb} {utxo} h') - $ to ∈-∩ (res-comp-domᵐ h₁ , h₂) - newBal' : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXO⦈ - ⟦ utxo' , fees' , deposits' , donations' ⟧ - → consumed pp utxoSt txb ≡ produced pp utxoSt txb - newBal' (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ x _ _ _ _ _ _ _ _ _ _ _) = x - newBal : consumed pp utxoSt txb ≡ produced pp utxoSt txb - newBal = newBal' step - noMintAda' : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXO⦈ - ⟦ utxo' , fees' , deposits' , donations' ⟧ - → coin (mint) ≡ 0 - noMintAda' (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ x _ _ _ _ _ _ _ _ _ _) = x - noMintAda : coin mint ≡ 0 - noMintAda = noMintAda' step - remDepTot : Coin - remDepTot = getCoin deposits - ref - - deposits-change' : Δdep ≡ tot - ref - deposits-change' = sym posPart-negPart≡x - - dep-ref : tot ≡ 0 → uDep + ref ≡ dep - dep-ref tot≡0 = ℤ.+-injective $ begin - ℤ.+_ (uDep + ref) ≡⟨ ℤ.pos-+ uDep ref ⟩ - ℤ.+_ uDep ℤ.+ (ref - 0) ≡˘⟨ cong (λ u → ℤ.+_ uDep ℤ.+ (ref - u)) tot≡0 ⟩ - ℤ.+_ uDep ℤ.+ (ref - tot) ≡⟨ cong ((ℤ.+ uDep) +_) (ℤ.⊖-swap ref tot) ⟩ - ℤ.+_ uDep ℤ.- (tot - ref) ≡˘⟨ cong (λ u → ℤ.+_ uDep ℤ.- u) deposits-change' ⟩ - ℤ.+_ uDep ℤ.- Δdep ≡˘⟨ cong ((ℤ.+ uDep) +_) (ℤ.⊖-swap dep uDep) ⟩ - ℤ.+_ uDep + (dep - uDep) ≡⟨ ℤ.distribʳ-⊖-+-pos uDep dep uDep ⟩ - (uDep + dep) - uDep ≡⟨ cong (_- uDep) (+-comm uDep dep) ⟩ - (dep + uDep) - uDep ≡˘⟨ ℤ.distribʳ-⊖-+-pos dep uDep uDep ⟩ - ℤ.+_ dep ℤ.+ (uDep - uDep) ≡⟨ cong (λ u → ℤ.+_ dep ℤ.+ u) (ℤ.n⊖n≡0 uDep) ⟩ - ℤ.+_ dep ℤ.+ ℤ.0ℤ ≡⟨ ℤ.+-identityʳ _ ⟩ - ℤ.+_ dep ∎ - - ref-tot-0 : ref ≢ 0 → tot ≡ 0 - ref-tot-0 ref≢0 with Δdep - ... | ℤ.+_ n = ⊥-elim (ref≢0 refl) - ... | ℤ.negsuc n = refl - - ref≤dep : ref ≤ dep - ref≤dep with ref ≟ 0 - ... | no ¬p = ≤″⇒≤ $ _ ,≤_ $ begin - ref + uDep ≡⟨ +-comm ref uDep ⟩ - uDep + ref ≡⟨ dep-ref $ ref-tot-0 ¬p ⟩ - dep ∎ - ... | yes p rewrite p = z≤n - - deposits-change : uDep ≡ dep + tot - ref - deposits-change = ℤ.+-injective $ begin - ℤ.+_ uDep ≡˘⟨ ℤ.+-identityʳ _ ⟩ - ℤ.+_ uDep ℤ.+ ℤ.0ℤ ≡˘⟨ cong! (ℤ.+-inverseˡ (ℤ.+_ dep)) ⟩ - ℤ.+_ uDep ℤ.+ (ℤ.-_ (ℤ.+_ dep) ℤ.+ (ℤ.+_ dep)) - ≡˘⟨ ℤ.+-assoc (ℤ.+_ uDep) (ℤ.-_ (ℤ.+_ dep)) (ℤ.+_ dep) ⟩ - (ℤ.+_ uDep ℤ.- (ℤ.+_ dep)) ℤ.+ (ℤ.+_ dep) ≡⟨ cong! (ℤ.m-n≡m⊖n uDep dep) ⟩ - Δdep ℤ.+ (ℤ.+_ dep) ≡⟨ ℤ.+-comm Δdep (ℤ.+_ dep) ⟩ - (ℤ.+_ dep) ℤ.+ Δdep ≡⟨ cong! deposits-change' ⟩ - (ℤ.+_ dep) ℤ.+ (tot - ref) ≡⟨ ℤ.distribʳ-⊖-+-pos dep tot ref ⟩ - (dep + tot) - ref ≡⟨ ℤ.⊖-≥ (m≤n⇒m≤n+o tot ref≤dep) ⟩ - ℤ.+_ (dep + tot - ref) ∎ - - split-balance : ∀ keys → cbalance utxo ≡ cbalance (utxo ∣ keys ᶜ) + cbalance (utxo ∣ keys) - split-balance keys = begin - cbalance utxo - ≡˘⟨ balance-cong-coin {utxo = (utxo ∣ keys ᶜ) ∪ˡ (utxo ∣ keys)}{utxo} - $ disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint) - ≡ᵉ-∘ ∪-sym - ≡ᵉ-∘ res-ex-∪ (_∈? keys) ⟩ - cbalance ((utxo ∣ keys ᶜ) ∪ˡ (utxo ∣ keys)) - ≡⟨ balance-∪ {utxo ∣ keys ᶜ} {utxo ∣ keys} $ flip res-ex-disjoint ⟩ - cbalance (utxo ∣ keys ᶜ) + cbalance (utxo ∣ keys) - ∎ - where open IsEquivalence ≡ᵉ-isEquivalence renaming (trans to infixl 4 _≡ᵉ-∘_) - - module _ (balanceUtxo balanceIns balanceNoIns balanceOuts balanceUtxo' : Coin) - (ref txFee txDonation tot : Coin) - (splitUtxo : balanceUtxo ≡ balanceNoIns + balanceIns) - (splitUtxo' : balanceUtxo' ≡ balanceNoIns + balanceOuts) - (balanced : balanceIns + ref + wdls ≡ balanceOuts + txFee + tot + txDonation) where - - utxo-ref-prop-worker : - balanceUtxo + ref + wdls ≡ balanceUtxo' + txFee + txDonation + tot - utxo-ref-prop-worker = begin - balanceUtxo + ref + wdls - ≡⟨ cong (λ u → u + ref + wdls) splitUtxo ⟩ - balanceNoIns ℕ.+ balanceIns ℕ.+ ref ℕ.+ wdls - ≡t⟨⟩ - balanceNoIns ℕ.+ (balanceIns ℕ.+ ref ℕ.+ wdls) - ≡⟨ cong (balanceNoIns +_) balanced ⟩ - balanceNoIns ℕ.+ (balanceOuts ℕ.+ txFee ℕ.+ tot ℕ.+ txDonation) - ≡t⟨⟩ - (balanceNoIns ℕ.+ balanceOuts ℕ.+ txFee) ℕ.+ tot ℕ.+ txDonation - ≡˘⟨ cong (λ x → (x + txFee) + tot + txDonation) splitUtxo' ⟩ - (balanceUtxo' ℕ.+ txFee) ℕ.+ tot ℕ.+ txDonation - ≡t⟨⟩ - balanceUtxo' ℕ.+ txFee ℕ.+ (tot ℕ.+ txDonation) - ≡⟨ cong (balanceUtxo' + txFee +_) $ +-comm tot txDonation ⟩ - balanceUtxo' ℕ.+ txFee ℕ.+ (txDonation ℕ.+ tot) - ≡t⟨⟩ - (balanceUtxo' ℕ.+ txFee) ℕ.+ txDonation ℕ.+ tot - ∎ - - utxo-ref-prop : - cbalance utxo + ref + wdls ≡ - cbalance ((utxo ∣ txIns ᶜ) ∪ˡ outs txb) + txFee + txDonation + tot - utxo-ref-prop = utxo-ref-prop-worker - (cbalance utxo) - (cbalance (utxo ∣ txIns)) - (cbalance (utxo ∣ txIns ᶜ)) - (cbalance (outs txb)) - (cbalance ((utxo ∣ txIns ᶜ) ∪ˡ outs txb)) - ref txFee txDonation tot - (split-balance txIns) - (balance-∪ {utxo ∣ txIns ᶜ} {outs txb} h) - (balValueToCoin {txb} {utxoSt} {UTxOEnv.pparams Γ} noMintAda newBal) - - rearrange0 : - (bal : ℕ) - → deposits' ≡ updateDeposits pp txb deposits - → bal + txFee + txDonation + tot + (remDepTot + fees) - ≡ bal + (fees + txFee + getCoin deposits' + txDonation) - rearrange0 bal h = begin - bal ℕ.+ txFee ℕ.+ txDonation ℕ.+ tot ℕ.+ (remDepTot ℕ.+ fees) - ≡t⟨⟩ - bal ℕ.+ (txFee ℕ.+ txDonation ℕ.+ (tot ℕ.+ remDepTot) ℕ.+ fees) - ≡⟨ cong (bal +_) $ begin - txFee + txDonation + (tot + remDepTot) + fees - ≡⟨ +-comm _ fees ⟩ - fees ℕ.+ (txFee ℕ.+ txDonation ℕ.+ (tot ℕ.+ remDepTot)) - ≡t⟨⟩ - (fees ℕ.+ txFee) ℕ.+ (txDonation ℕ.+ (tot ℕ.+ remDepTot)) - ≡⟨ cong ((fees + txFee) +_) $ +-comm txDonation (tot + remDepTot) ⟩ - (fees + txFee) ℕ.+ ((tot + remDepTot) ℕ.+ txDonation) - ≡t⟨⟩ - (fees + txFee) ℕ.+ (tot + remDepTot) ℕ.+ txDonation - ≡⟨ cong (λ x → (fees + txFee) + x + txDonation) - $ begin tot + (dep - ref) ≡˘⟨ +-∸-assoc tot ref≤dep ⟩ - (tot + dep) - ref ≡⟨ cong (_- ref) $ +-comm tot dep ⟩ - (dep + tot) - ref ≡˘⟨ deposits-change ⟩ - uDep ≡⟨ cong getCoin $ sym h ⟩ - getCoin deposits' ∎ ⟩ - (fees + txFee) + getCoin deposits' + txDonation - ∎ ⟩ - bal + ((fees + txFee) + getCoin deposits' + txDonation) - ∎ - - module _ (balanceUtxo balanceUtxo' : Coin) - (ref-prop : balanceUtxo + ref + wdls ≡ balanceUtxo' + txFee + txDonation + tot) - (h : deposits' ≡ updateDeposits pp txb deposits) - where - - pov-scripts-worker : isValid ≡ true - → balanceUtxo + fees + getCoin deposits + donations + wdls * χ(isValid) - ≡ balanceUtxo' + (fees + txFee) + getCoin deposits' + (donations + txDonation) - pov-scripts-worker valid = begin - balanceUtxo + fees + dep + donations + wdls * χ(isValid) - ≡⟨ cong (λ x → balanceUtxo + fees + dep + donations + wdls * χ x) valid ⟩ - balanceUtxo + fees + dep + donations + wdls * 1 - ≡⟨ cong (balanceUtxo + fees + dep + donations +_) (*-identityʳ wdls) ⟩ - balanceUtxo + fees + dep + donations + wdls - ≡⟨ +-assoc (balanceUtxo + fees + dep) donations wdls ⟩ - balanceUtxo + fees + dep + (donations + wdls) - ≡⟨ cong (balanceUtxo + fees + dep +_) (+-comm donations wdls) ⟩ - balanceUtxo + fees + dep + (wdls + donations) - ≡˘⟨ +-assoc (balanceUtxo + fees + dep) wdls donations ⟩ - balanceUtxo + fees + dep + wdls + donations - ≡⟨ cong (_+ donations) - $ begin - balanceUtxo + fees + dep + wdls - ≡˘⟨ cong (λ x → balanceUtxo + fees + x + wdls) (m+[n∸m]≡n ref≤dep) ⟩ - balanceUtxo + fees + (ref + remDepTot) + wdls - ≡⟨ cong (_+ wdls) (+-assoc balanceUtxo fees (ref + remDepTot)) ⟩ - balanceUtxo + (fees + (ref + remDepTot)) + wdls - ≡⟨ cong (λ x → balanceUtxo + x + wdls) (+-comm fees (ref + remDepTot)) ⟩ - balanceUtxo + (ref + remDepTot + fees) + wdls - ≡⟨ cong (λ x → balanceUtxo + x + wdls) (+-assoc ref remDepTot fees) ⟩ -- - balanceUtxo + (ref + (remDepTot + fees)) + wdls - ≡⟨ +-assoc balanceUtxo (ref + (remDepTot + fees)) wdls ⟩ -- - balanceUtxo + (ref + (remDepTot + fees) + wdls) - ≡⟨ cong (balanceUtxo +_) (+-assoc ref (remDepTot + fees) wdls) ⟩ - balanceUtxo + (ref + ((remDepTot + fees) + wdls)) - ≡⟨ cong (λ x → balanceUtxo + (ref + x)) (+-comm (remDepTot + fees) wdls) ⟩ - balanceUtxo + (ref + (wdls + (remDepTot + fees))) - ≡˘⟨ +-assoc balanceUtxo ref (wdls + (remDepTot + fees)) ⟩ - balanceUtxo + ref + (wdls + (remDepTot + fees)) - ≡˘⟨ +-assoc (balanceUtxo + ref) wdls (remDepTot + fees) ⟩ - balanceUtxo + ref + wdls + (remDepTot + fees) - ≡⟨ cong (_+ (remDepTot + fees)) ref-prop ⟩ - balanceUtxo' + txFee + txDonation + tot + (remDepTot + fees) - ≡⟨ rearrange0 (balanceUtxo') h ⟩ - balanceUtxo' + (fees + txFee + getCoin deposits' + txDonation) - ∎ ⟩ - balanceUtxo' ℕ.+ (fees + txFee ℕ.+ getCoin deposits' ℕ.+ txDonation) ℕ.+ donations - ≡t⟨⟩ - balanceUtxo' ℕ.+ (fees + txFee) ℕ.+ getCoin deposits' ℕ.+ (txDonation ℕ.+ donations) - ≡⟨ cong (balanceUtxo' + (fees + txFee) + getCoin deposits' ℕ.+_) - $ +-comm txDonation donations ⟩ - balanceUtxo' + (fees + txFee) + getCoin deposits' + (donations + txDonation) - ∎ - - pov-scripts : deposits' ≡ updateDeposits pp txb deposits - → isValid ≡ true - → cbalance utxo + fees + dep + donations + wdls * χ(isValid) - ≡ cbalance ((utxo ∣ txIns ᶜ) ∪ˡ outs txb) - + (fees + txFee) + getCoin deposits' + (donations + txDonation) - pov-scripts h valid = pov-scripts-worker (cbalance utxo) (cbalance ((utxo ∣ txIns ᶜ) ∪ˡ outs txb)) utxo-ref-prop h valid - - pov-no-scripts : isValid ≡ false - → cbalance utxo + fees + dep + donations + wdls * χ(isValid) - ≡ cbalance (utxo ∣ collateralInputs ᶜ) + (fees + cbalance (utxo ∣ collateralInputs)) + dep + donations - pov-no-scripts invalid = begin - cbalance utxo + fees + dep + donations + wdls * χ(isValid) ≡⟨ cong (λ x → cbalance utxo + fees + dep + donations + wdls * χ x) invalid ⟩ - cbalance utxo + fees + dep + donations + wdls * 0 ≡⟨ cong (cbalance utxo + fees + dep + donations +_ ) (*-zeroʳ wdls) ⟩ - cbalance utxo + fees + dep + donations + 0 ≡⟨ +-identityʳ _ ⟩ - cbalance utxo + fees + dep + donations ≡⟨ cong (λ x → x + dep + donations) $ begin - cbalance utxo ℕ.+ fees ≡⟨ cong (_+ fees) (split-balance collateralInputs) ⟩ - cbalance (utxo ∣ collateralInputs ᶜ) ℕ.+ cbalance (utxo ∣ collateralInputs) ℕ.+ fees ≡t⟨⟩ - cbalance (utxo ∣ collateralInputs ᶜ) ℕ.+ (cbalance (utxo ∣ collateralInputs) ℕ.+ fees) ≡⟨ cong (cbalance (utxo ∣ collateralInputs ᶜ) +_) (+-comm _ fees) ⟩ - cbalance (utxo ∣ collateralInputs ᶜ) ℕ.+ (fees ℕ.+ cbalance (utxo ∣ collateralInputs)) ∎ ⟩ - cbalance (utxo ∣ collateralInputs ᶜ) + (fees + cbalance (utxo ∣ collateralInputs)) + dep + donations - ∎ \end{code} Here we state the fact that the UTxO relation is computable. @@ -555,157 +160,3 @@ UTXO-step-computes-UTXO = ≡-success⇔STS ⦃ Computational-UTXO ⦄ \caption{Computing the UTXO transition system} \end{figure*} - -\begin{property}[\textbf{General Minimum Spending Condition}]~\\ - -\begin{code}[hide] -isRefundCert : DCert → Bool -isRefundCert (dereg c _) = true -isRefundCert (deregdrep c _) = true -isRefundCert _ = false - -noRefundCert : List DCert → Type _ -noRefundCert l = All (λ cert → isRefundCert cert ≡ false) l - -opaque - unfolding List-Model - unfolding finiteness - fin∘list[] : {A : Type} → proj₁ (finiteness{A = A} ∅) ≡ [] - fin∘list[] = refl - fin∘list∷[] : {A : Type} {a : A} → proj₁ (finiteness ❴ a ❵) ≡ [ a ] - fin∘list∷[] = refl - -coin∅ : getCoin{A = Deposits} ∅ ≡ 0 -coin∅ = begin - foldr (λ x → (proj₂ x) +_) 0 (deduplicate _≟_ (proj₁ (finiteness ∅))) - ≡⟨ cong (λ u → (foldr (λ x → (proj₂ x) +_) 0 (deduplicate _≟_ u))) fin∘list[] ⟩ - foldr (λ (x : DepositPurpose × Coin) → (proj₂ x) +_) 0 (deduplicate _≟_ []) - ≡⟨ cong (λ u → (foldr (λ (x : DepositPurpose × Coin) → (proj₂ x) +_) 0 u)) - {x = deduplicate _≟_ []} {y = []} refl ⟩ - foldr (λ (x : DepositPurpose × Coin) → (proj₂ x) +_) 0 [] - ≡⟨ refl ⟩ - 0 ∎ - where open Prelude.≡-Reasoning - -getCoin-singleton : ((dp , c) : DepositPurpose × Coin) → indexedSumᵛ' id ❴ (dp , c) ❵ ≡ c -getCoin-singleton _ = indexedSum-singleton' {A = DepositPurpose × Coin} {f = proj₂} (finiteness _) - -module _ -- ASSUMPTION -- - (gc-hom : (d₁ d₂ : Deposits) → getCoin (d₁ ∪⁺ d₂) ≡ getCoin d₁ + getCoin d₂) - where - ∪⁺singleton≡ : {deps : Deposits} {(dp , c) : DepositPurpose × Coin} - → getCoin (deps ∪⁺ ❴ (dp , c) ❵ᵐ) ≡ getCoin deps + c - ∪⁺singleton≡ {deps} {(dp , c)} = begin - getCoin (deps ∪⁺ ❴ (dp , c) ❵) - ≡⟨ gc-hom deps ❴ (dp , c) ❵ ⟩ - getCoin deps + getCoin{A = Deposits} ❴ (dp , c) ❵ - ≡⟨ cong (getCoin deps +_) (getCoin-singleton (dp , c)) ⟩ - getCoin deps + c - ∎ - where open Prelude.≡-Reasoning - - module _ {deposits : Deposits} {txid : TxId} {gaDep : Coin} where - - ≤updatePropDeps : (props : List GovProposal) - → getCoin deposits ≤ getCoin (updateProposalDeposits props txid gaDep deposits) - ≤updatePropDeps [] = ≤-reflexive refl - ≤updatePropDeps (x ∷ props) = ≤-trans (≤updatePropDeps props) - (≤-trans (m≤m+n _ _) - (≤-reflexive $ sym $ ∪⁺singleton≡)) - updatePropDeps≡ : (ps : List GovProposal) - → getCoin (updateProposalDeposits ps txid gaDep deposits) - getCoin deposits ≡ (length ps) * gaDep - updatePropDeps≡ [] = n∸n≡0 (getCoin deposits) - updatePropDeps≡ (_ ∷ ps) = let - upD = updateProposalDeposits ps txid gaDep deposits in - begin - getCoin (upD ∪⁺ ❴ GovActionDeposit (txid , length ps) , gaDep ❵ᵐ) ∸ getCoin deposits - ≡⟨ cong (_∸ getCoin deposits) ∪⁺singleton≡ ⟩ - getCoin upD + gaDep ∸ getCoin deposits - ≡⟨ +-∸-comm _ (≤updatePropDeps ps) ⟩ - (getCoin upD ∸ getCoin deposits) + gaDep - ≡⟨ cong (_+ gaDep) (updatePropDeps≡ ps) ⟩ - (length ps) * gaDep + gaDep - ≡⟨ +-comm ((length ps) * gaDep) gaDep ⟩ - gaDep + (length ps) * gaDep - ∎ - where open Prelude.≡-Reasoning - - ≤certDeps : {d : Deposits} {(dp , c) : DepositPurpose × Coin} - → getCoin d ≤ getCoin (d ∪⁺ ❴ (dp , c) ❵) - - ≤certDeps {d} = begin - getCoin d ≤⟨ m≤m+n (getCoin d) _ ⟩ - getCoin d + _ ≡⟨ sym ∪⁺singleton≡ ⟩ - getCoin (d ∪⁺ ❴ _ ❵) ∎ - where open ≤-Reasoning - - - ≤updateCertDeps : (cs : List DCert) {pp : PParams} {deposits : Deposits} - → noRefundCert cs - → getCoin deposits ≤ getCoin (updateCertDeposits pp cs deposits) - ≤updateCertDeps [] nrf = ≤-reflexive refl - ≤updateCertDeps (reg c v ∷ cs) {pp} {deposits} (_ All.∷ nrf) = - ≤-trans ≤certDeps (≤updateCertDeps cs {pp} {deposits ∪⁺ ❴ CredentialDeposit c , pp .PParams.keyDeposit ❵} nrf) - ≤updateCertDeps (delegate c _ _ v ∷ cs) {pp} {deposits} (_ All.∷ nrf) = - ≤-trans ≤certDeps (≤updateCertDeps cs {pp} {deposits ∪⁺ ❴ CredentialDeposit c , v ❵} nrf) - ≤updateCertDeps (regpool _ _ ∷ cs) (_ All.∷ nrf) = ≤-trans ≤certDeps (≤updateCertDeps cs nrf) - ≤updateCertDeps (retirepool _ _ ∷ cs) (_ All.∷ nrf) = ≤updateCertDeps cs nrf - ≤updateCertDeps (regdrep _ _ _ ∷ cs) (_ All.∷ nrf) = ≤-trans ≤certDeps (≤updateCertDeps cs nrf) - ≤updateCertDeps (ccreghot _ _ ∷ cs) (_ All.∷ nrf) = ≤updateCertDeps cs nrf - - -- Main Theorem: General Minimum Spending Condition -- - gmsc : let open Tx tx renaming (body to txb); open TxBody txb - pp = UTxOEnv.pparams Γ; open PParams pp - open UTxOState utxoState - renaming (utxo to st; fees to fs; deposits to deps; donations to dons) - in - Γ ⊢ ⟦ st , fs , deps , dons ⟧ ⇀⦇ tx ,UTXO⦈ - ⟦ utxo' , fees' , deposits' , donations' ⟧ - - → noRefundCert txCerts -- FINAL ASSUMPTION -- - - ------------------------------------------------------------------- - → coin (consumed pp utxoState txb) ≥ length txGovProposals * govActionDeposit - - gmsc step@(UTXO-inductive⋯ tx Γ utxoState _ _ _ _ _ _ c≡p cmint≡0 _ _ _ _ _ _ _ _ _ _) nrf = - begin - length txGovProposals * govActionDeposit - ≡˘⟨ updatePropDeps≡ txGovProposals ⟩ - getCoin (updateProposalDeposits txGovProposals txId govActionDeposit deps) ∸ getCoin deps - ≤⟨ ∸-monoˡ-≤ (getCoin deps) (≤updateCertDeps txCerts nrf) ⟩ - getCoin (updateDeposits pp txb deps) - getCoin deps - ≡⟨ ∸≡posPart⊖ {getCoin (updateDeposits pp txb deps)} {getCoin deps} ⟩ - newDeps - ≤⟨ m≤n+m newDeps (coin balOut + txFee + txDonation) ⟩ - coin balOut + txFee + txDonation + newDeps - ≡⟨ +-assoc (coin balOut + txFee) txDonation newDeps ⟩ - coin balOut + txFee + (txDonation + newDeps) - ≡⟨ cong (coin balOut + txFee +_) (+-comm txDonation newDeps) ⟩ - coin balOut + txFee + (newDeps + txDonation) - ≡˘⟨ +-assoc (coin balOut + txFee) newDeps txDonation ⟩ - coin balOut + txFee + newDeps + txDonation - ≡˘⟨ cong (λ x → x + newDeps + txDonation) coin-inject-lemma ⟩ - coin (balOut + inject txFee) + newDeps + txDonation - ≡˘⟨ cong (_+ txDonation) coin-inject-lemma ⟩ - coin (balOut + inject txFee + inject newDeps) + txDonation - ≡˘⟨ coin-inject-lemma ⟩ - coin (balOut + inject txFee + inject newDeps + inject txDonation) - ≡˘⟨ cong coin c≡p ⟩ - coin (balIn + mint + inject refunds + inject wdrls) ∎ - where - open ≤-Reasoning - pp : PParams - pp = UTxOEnv.pparams Γ; open PParams pp - open Tx tx renaming (body to txb); open TxBody txb - open UTxOState utxoState renaming (utxo to st; fees to fs; deposits to deps; donations to dons) - - newDeps refunds wdrls : Coin - newDeps = newDeposits pp utxoState txb - refunds = depositRefunds pp utxoState txb - wdrls = getCoin txWithdrawals - - balIn balOut : Value - balIn = balance (st ∣ txIns) - balOut = balance (outs txb) -\end{code} -\end{property} diff --git a/src/Ledger/Conway/Specification/Utxo/Properties/DepositHelpers.agda b/src/Ledger/Conway/Specification/Utxo/Properties/DepositHelpers.agda new file mode 100644 index 000000000..00a49f9e6 --- /dev/null +++ b/src/Ledger/Conway/Specification/Utxo/Properties/DepositHelpers.agda @@ -0,0 +1,422 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Conway.Specification.Abstract +open import Ledger.Conway.Specification.Transaction + +module Ledger.Conway.Specification.Utxo.Properties.DepositHelpers + (txs : _) (open TransactionStructure txs) + (abs : AbstractFunctions txs) (open AbstractFunctions abs) + where + +open import Prelude; open Equivalence +open import Ledger.Prelude hiding (≤-trans; ≤-antisym; All); open Properties +open import Ledger.Conway.Specification.Certs govStructure +open import Ledger.Conway.Specification.Utxo txs abs + +open import Tactic.EquationalReasoning using (module ≡-Reasoning) +open import Tactic.Cong using (cong!) +open import stdlib-meta.Tactic.MonoidSolver.NonNormalising using (solve-macro) + +open import Data.Nat.Properties hiding (_≟_) +import Data.Nat as ℕ +import Data.Integer as ℤ +open import Data.Integer.Properties as Int + using ( +-injective; n⊖n≡0; distribʳ-⊖-+-pos; ⊖-swap; pos-+; ⊖-≥ + ; m-n≡m⊖n; +-inverseˡ) + +open import Relation.Binary using (IsEquivalence) + +open import Algebra.Morphism using (module MonoidMorphisms; IsMagmaHomomorphism) +open import Algebra.Definitions.RawMagma +-rawMagma using () renaming (_,_ to _,≤_) + + +posPart-negPart≡x : {x : ℤ} → posPart x - negPart x ≡ x +posPart-negPart≡x {ℤ.+_ n} = refl +posPart-negPart≡x {ℤ.negsuc n} = refl + +χ : Bool → ℕ +χ false = 0 +χ true = 1 + +open MonoidMorphisms.IsMonoidHomomorphism +private + ∙-homo-Coin = IsMagmaHomomorphism.homo (isMagmaHomomorphism coinIsMonoidHomomorphism) + +module _ + {txb : _} (open TxBody txb) + {utxo : UTxO} + where + opaque + unfolding outs + open Tactic.EquationalReasoning.≡-Reasoning {A = ℕ} (solve-macro (quoteTerm +-0-monoid)) + + newTxid⇒disj : txId ∉ mapˢ proj₁ (dom utxo) + → disjoint' (dom utxo) (dom (outs txb)) + newTxid⇒disj id∉utxo = disjoint⇒disjoint' λ h h' → id∉utxo $ to ∈-map + (-, (case from ∈-map h' of λ where + (_ , refl , h'') → case from ∈-map h'' of λ where (_ , refl , _) → refl) , h) + + consumedCoinEquality : ∀ {utxoState} {pp} + → coin mint ≡ 0 + → coin (consumed pp utxoState txb) + ≡ cbalance ((UTxOState.utxo utxoState) ∣ txIns) + depositRefunds pp utxoState txb + getCoin txWithdrawals + consumedCoinEquality {utxoState} {pp} h = + let utxo = UTxOState.utxo utxoState + dRefs = depositRefunds pp utxoState txb + sWdls = getCoin txWithdrawals + in begin + coin (balance (utxo ∣ txIns) + mint + inject dRefs + inject sWdls) + ≡⟨ ∙-homo-Coin _ _ ⟩ + coin (balance (utxo ∣ txIns) + mint + inject dRefs) + coin (inject $ sWdls) + ≡⟨ cong (coin (balance (utxo ∣ txIns) + mint + inject dRefs) +_) (coin∘inject≗id _) ⟩ + coin (balance (utxo ∣ txIns) + mint + inject dRefs) + sWdls + ≡⟨ cong (_+ sWdls) (∙-homo-Coin _ _) ⟩ + coin (balance (utxo ∣ txIns) + mint) + coin (inject $ dRefs) + sWdls + ≡⟨ cong (λ u → coin (balance (utxo ∣ txIns) + mint) + u + sWdls) (coin∘inject≗id _) ⟩ + coin (balance (utxo ∣ txIns) + mint) + dRefs + sWdls + ≡⟨ cong (λ u → u + dRefs + sWdls) (∙-homo-Coin _ _) ⟩ + cbalance (utxo ∣ txIns) + coin mint + dRefs + sWdls + ≡⟨ cong (λ x → cbalance (utxo ∣ txIns) + x + dRefs + sWdls) h ⟩ + cbalance (utxo ∣ txIns) + 0 + dRefs + sWdls + ≡⟨ cong (λ x → x + dRefs + sWdls) (+-identityʳ (cbalance (utxo ∣ txIns))) ⟩ + cbalance (utxo ∣ txIns) + dRefs + sWdls + ∎ + + producedCoinEquality : ∀ {utxoState} {pp} + → coin (produced pp utxoState txb) + ≡ cbalance (outs txb) + txFee + newDeposits pp utxoState txb + txDonation + producedCoinEquality {utxoState} {pp} = + begin + coin (balance (outs txb) + inject txFee + + inject (newDeposits pp utxoState txb) + inject txDonation) + ≡⟨ ∙-homo-Coin _ _ ⟩ + coin (balance (outs txb) + inject txFee + + inject (newDeposits pp utxoState txb)) + coin (inject txDonation) + ≡⟨ cong (_+ coin (inject txDonation)) (begin + coin (balance (outs txb) + inject txFee + + inject (newDeposits pp utxoState txb)) + ≡⟨ ∙-homo-Coin _ _ ⟩ + coin (balance (outs txb) +ᵛ inject txFee) + ℕ.+ coin (inject (newDeposits pp utxoState txb)) + ≡⟨ cong! (coin∘inject≗id _) ⟩ + coin (balance (outs txb) +ᵛ inject txFee) + ℕ.+ newDeposits pp utxoState txb + ≡⟨ cong! (∙-homo-Coin _ _) ⟩ + coin (balance (outs txb)) ℕ.+ coin (inject txFee) + ℕ.+ newDeposits pp utxoState txb + ≡⟨ cong (λ x → cbalance (outs txb) + x + newDeposits pp utxoState txb) + $ coin∘inject≗id txFee ⟩ + cbalance (outs txb) + txFee + newDeposits pp utxoState txb + ∎ + )⟩ + cbalance (outs txb) + txFee + + newDeposits pp utxoState txb + coin (inject txDonation) + ≡⟨ cong (cbalance (outs txb) + txFee + newDeposits pp utxoState txb +_) + $ coin∘inject≗id _ ⟩ + cbalance (outs txb) + txFee + newDeposits pp utxoState txb + txDonation + ∎ + + balValueToCoin : ∀ {utxoState} {pp} + → coin mint ≡ 0 + → consumed pp utxoState txb ≡ produced pp utxoState txb + → cbalance ((UTxOState.utxo utxoState) ∣ txIns) + + depositRefunds pp utxoState txb + getCoin txWithdrawals + ≡ cbalance (outs txb) + txFee + newDeposits pp utxoState txb + txDonation + balValueToCoin {utxoState} {pp} h h' = begin + cbalance ((UTxOState.utxo utxoState) ∣ txIns) + depositRefunds pp utxoState txb + getCoin txWithdrawals + ≡˘⟨ consumedCoinEquality {utxoState} {pp} h ⟩ + coin (consumed pp utxoState txb) + ≡⟨ cong! h' ⟩ + coin (produced pp utxoState txb) + ≡⟨ producedCoinEquality {utxoState} {pp} ⟩ + cbalance (outs txb) + txFee + newDeposits pp utxoState txb + txDonation + ∎ + +module _ {utxo utxo' : UTxO} where + + opaque + unfolding balance + balance-cong : ∣ utxo ∣ ≡ᵉ ∣ utxo' ∣ → balance utxo ≈ balance utxo' + balance-cong eq = indexedSumᵐ-cong {M = Value} {x = (mapValues txOutHash utxo) ᶠᵐ} {(mapValues txOutHash utxo') ᶠᵐ} (map-≡ᵉ eq) + + balance-cong-coin : ∣ utxo ∣ ≡ᵉ ∣ utxo' ∣ → cbalance utxo ≡ cbalance utxo' + balance-cong-coin x = + coinIsMonoidHomomorphism .⟦⟧-cong (balance-cong x) + where open MonoidMorphisms.IsMonoidHomomorphism + + balance-∪ : disjoint (dom utxo) (dom utxo') + → cbalance (utxo ∪ˡ utxo') ≡ cbalance utxo + cbalance utxo' + balance-∪ h = begin + cbalance (utxo ∪ˡ utxo') + ≡⟨ ⟦⟧-cong coinIsMonoidHomomorphism + $ indexedSumᵐ-cong {f = getValueʰ ∘ proj₂} {x = (mapValues txOutHash (utxo ∪ˡ utxo')) ᶠᵐ} {((mapValues txOutHash utxo) ᶠᵐ) ∪ˡᶠ ((mapValues txOutHash utxo') ᶠᵐ)} (disjoint-∪ˡ-mapValues {M = utxo} {utxo'} _ h) + ⟩ + coin (indexedSumᵐ _ (((mapValues txOutHash utxo) ᶠᵐ) ∪ˡᶠ ((mapValues txOutHash utxo') ᶠᵐ))) + ≡⟨ ⟦⟧-cong coinIsMonoidHomomorphism + $ indexedSumᵐ-∪ {M = Value} {X = (mapValues txOutHash utxo) ᶠᵐ} {(mapValues txOutHash utxo') ᶠᵐ} + (λ x x₁ → h (dom-mapʳ⊆ x) (dom-mapʳ⊆ x₁)) + ⟩ + coin (balance utxo + balance utxo') + ≡⟨ ∙-homo-Coin _ _ ⟩ + cbalance utxo + cbalance utxo' + ∎ + where open Tactic.EquationalReasoning.≡-Reasoning {A = ℕ} (solve-macro (quoteTerm +-0-monoid)) + + +module _ + {utxo utxo' : UTxO} + {fees fees' : Fees} + {deposits deposits' : Deposits} + {donations donations' : Donations} + {tx : Tx} (let open Tx tx renaming (body to txb); open TxBody txb) + {Γ : UTxOEnv} + (step : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXO⦈ + ⟦ utxo' , fees' , deposits' , donations' ⟧) + (h' : txId ∉ mapˢ proj₁ (dom utxo)) + where + open Tactic.EquationalReasoning.≡-Reasoning {A = ℕ} (solve-macro (quoteTerm +-0-monoid)) + + private + stepS : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXOS⦈ + ⟦ utxo' , fees' , deposits' , donations' ⟧ + stepS = case step of λ where + (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) → h + + pp : PParams + pp = UTxOEnv.pparams Γ + dep : Coin + dep = getCoin deposits + uDep : Coin + uDep = getCoin (updateDeposits pp txb deposits) + Δdep : ℤ + Δdep = depositsChange pp txb deposits + utxoSt : UTxOState + utxoSt = ⟦ utxo , fees , deposits , donations ⟧ + ref tot : Coin + ref = depositRefunds pp utxoSt txb + wdls = getCoin txWithdrawals + tot = newDeposits pp utxoSt txb + h : disjoint (dom (utxo ∣ txIns ᶜ)) (dom (outs txb)) + h = λ h₁ h₂ → ∉-∅ $ proj₁ (newTxid⇒disj {txb} {utxo} h') + $ to ∈-∩ (res-comp-domᵐ h₁ , h₂) + newBal' : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXO⦈ + ⟦ utxo' , fees' , deposits' , donations' ⟧ + → consumed pp utxoSt txb ≡ produced pp utxoSt txb + newBal' (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ x _ _ _ _ _ _ _ _ _ _ _) = x + newBal : consumed pp utxoSt txb ≡ produced pp utxoSt txb + newBal = newBal' step + noMintAda' : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXO⦈ + ⟦ utxo' , fees' , deposits' , donations' ⟧ + → coin (mint) ≡ 0 + noMintAda' (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ x _ _ _ _ _ _ _ _ _ _) = x + noMintAda : coin mint ≡ 0 + noMintAda = noMintAda' step + remDepTot : Coin + remDepTot = getCoin deposits - ref + + deposits-change' : Δdep ≡ tot - ref + deposits-change' = sym posPart-negPart≡x + + dep-ref : tot ≡ 0 → uDep + ref ≡ dep + dep-ref tot≡0 = +-injective $ begin + ℤ.+_ (uDep + ref) ≡⟨ pos-+ uDep ref ⟩ + ℤ.+_ uDep ℤ.+ (ref - 0) ≡˘⟨ cong (λ u → ℤ.+_ uDep ℤ.+ (ref - u)) tot≡0 ⟩ + ℤ.+_ uDep ℤ.+ (ref - tot) ≡⟨ cong ((ℤ.+ uDep) +_) (⊖-swap ref tot) ⟩ + ℤ.+_ uDep ℤ.- (tot - ref) ≡˘⟨ cong (λ u → ℤ.+_ uDep ℤ.- u) deposits-change' ⟩ + ℤ.+_ uDep ℤ.- Δdep ≡˘⟨ cong ((ℤ.+ uDep) +_) (⊖-swap dep uDep) ⟩ + ℤ.+_ uDep + (dep - uDep) ≡⟨ Int.distribʳ-⊖-+-pos uDep dep uDep ⟩ + (uDep + dep) - uDep ≡⟨ cong (_- uDep) (+-comm uDep dep) ⟩ + (dep + uDep) - uDep ≡˘⟨ Int.distribʳ-⊖-+-pos dep uDep uDep ⟩ + -- ℤ.+_ uDep + (dep - uDep) ≡⟨ distribʳ-⊖-+-pos uDep dep uDep ⟩ + -- (uDep + dep) - uDep ≡⟨ cong (_- uDep) (+-comm uDep dep) ⟩ + -- (dep + uDep) - uDep ≡˘⟨ distribʳ-⊖-+-pos dep uDep uDep ⟩ + ℤ.+_ dep ℤ.+ (uDep - uDep) ≡⟨ cong (λ u → ℤ.+_ dep ℤ.+ u) (n⊖n≡0 uDep) ⟩ + ℤ.+_ dep ℤ.+ ℤ.0ℤ ≡⟨ Int.+-identityʳ _ ⟩ + ℤ.+_ dep ∎ + + ref-tot-0 : ref ≢ 0 → tot ≡ 0 + ref-tot-0 ref≢0 with Δdep + ... | ℤ.+_ n = ⊥-elim (ref≢0 refl) + ... | ℤ.negsuc n = refl + + ref≤dep : ref ≤ dep + ref≤dep with ref ≟ 0 + ... | no ¬p = ≤″⇒≤ $ _ ,≤_ $ begin + ref + uDep ≡⟨ +-comm ref uDep ⟩ + uDep + ref ≡⟨ dep-ref $ ref-tot-0 ¬p ⟩ + dep ∎ + ... | yes p rewrite p = z≤n + + deposits-change : uDep ≡ dep + tot - ref + deposits-change = +-injective $ begin + ℤ.+_ uDep ≡˘⟨ Int.+-identityʳ _ ⟩ + ℤ.+_ uDep ℤ.+ ℤ.0ℤ ≡˘⟨ cong! (+-inverseˡ (ℤ.+_ dep)) ⟩ + ℤ.+_ uDep ℤ.+ (ℤ.-_ (ℤ.+_ dep) ℤ.+ (ℤ.+_ dep)) + ≡˘⟨ Int.+-assoc (ℤ.+_ uDep) (ℤ.-_ (ℤ.+_ dep)) (ℤ.+_ dep) ⟩ + (ℤ.+_ uDep ℤ.- (ℤ.+_ dep)) ℤ.+ (ℤ.+_ dep) ≡⟨ cong! (m-n≡m⊖n uDep dep) ⟩ + Δdep ℤ.+ (ℤ.+_ dep) ≡⟨ Int.+-comm Δdep (ℤ.+_ dep) ⟩ + (ℤ.+_ dep) ℤ.+ Δdep ≡⟨ cong! deposits-change' ⟩ + (ℤ.+_ dep) ℤ.+ (tot - ref) ≡⟨ distribʳ-⊖-+-pos dep tot ref ⟩ + (dep + tot) - ref ≡⟨ ⊖-≥ (m≤n⇒m≤n+o tot ref≤dep) ⟩ + ℤ.+_ (dep + tot - ref) ∎ + + split-balance : ∀ keys → cbalance utxo ≡ cbalance (utxo ∣ keys ᶜ) + cbalance (utxo ∣ keys) + split-balance keys = begin + cbalance utxo + ≡˘⟨ balance-cong-coin {utxo = (utxo ∣ keys ᶜ) ∪ˡ (utxo ∣ keys)}{utxo} + $ disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint) + ≡ᵉ-∘ ∪-sym + ≡ᵉ-∘ res-ex-∪ (_∈? keys) ⟩ + cbalance ((utxo ∣ keys ᶜ) ∪ˡ (utxo ∣ keys)) + ≡⟨ balance-∪ {utxo ∣ keys ᶜ} {utxo ∣ keys} $ flip res-ex-disjoint ⟩ + cbalance (utxo ∣ keys ᶜ) + cbalance (utxo ∣ keys) + ∎ + where open IsEquivalence ≡ᵉ-isEquivalence renaming (trans to infixl 4 _≡ᵉ-∘_) + + module _ (balanceUtxo balanceIns balanceNoIns balanceOuts balanceUtxo' : Coin) + (ref txFee txDonation tot : Coin) + (splitUtxo : balanceUtxo ≡ balanceNoIns + balanceIns) + (splitUtxo' : balanceUtxo' ≡ balanceNoIns + balanceOuts) + (balanced : balanceIns + ref + wdls ≡ balanceOuts + txFee + tot + txDonation) where + + utxo-ref-prop-worker : + balanceUtxo + ref + wdls ≡ balanceUtxo' + txFee + txDonation + tot + utxo-ref-prop-worker = begin + balanceUtxo + ref + wdls + ≡⟨ cong (λ u → u + ref + wdls) splitUtxo ⟩ + balanceNoIns ℕ.+ balanceIns ℕ.+ ref ℕ.+ wdls + ≡t⟨⟩ + balanceNoIns ℕ.+ (balanceIns ℕ.+ ref ℕ.+ wdls) + ≡⟨ cong (balanceNoIns +_) balanced ⟩ + balanceNoIns ℕ.+ (balanceOuts ℕ.+ txFee ℕ.+ tot ℕ.+ txDonation) + ≡t⟨⟩ + (balanceNoIns ℕ.+ balanceOuts ℕ.+ txFee) ℕ.+ tot ℕ.+ txDonation + ≡˘⟨ cong (λ x → (x + txFee) + tot + txDonation) splitUtxo' ⟩ + (balanceUtxo' ℕ.+ txFee) ℕ.+ tot ℕ.+ txDonation + ≡t⟨⟩ + balanceUtxo' ℕ.+ txFee ℕ.+ (tot ℕ.+ txDonation) + ≡⟨ cong (balanceUtxo' + txFee +_) $ +-comm tot txDonation ⟩ + balanceUtxo' ℕ.+ txFee ℕ.+ (txDonation ℕ.+ tot) + ≡t⟨⟩ + (balanceUtxo' ℕ.+ txFee) ℕ.+ txDonation ℕ.+ tot + ∎ + + utxo-ref-prop : + cbalance utxo + ref + wdls ≡ + cbalance ((utxo ∣ txIns ᶜ) ∪ˡ outs txb) + txFee + txDonation + tot + utxo-ref-prop = utxo-ref-prop-worker + (cbalance utxo) + (cbalance (utxo ∣ txIns)) + (cbalance (utxo ∣ txIns ᶜ)) + (cbalance (outs txb)) + (cbalance ((utxo ∣ txIns ᶜ) ∪ˡ outs txb)) + ref txFee txDonation tot + (split-balance txIns) + (balance-∪ {utxo ∣ txIns ᶜ} {outs txb} h) + (balValueToCoin {utxo = utxo} {utxoSt} {UTxOEnv.pparams Γ} noMintAda newBal) + + rearrange0 : + (bal : ℕ) + → deposits' ≡ updateDeposits pp txb deposits + → bal + txFee + txDonation + tot + (remDepTot + fees) + ≡ bal + (fees + txFee + getCoin deposits' + txDonation) + rearrange0 bal h = begin + bal ℕ.+ txFee ℕ.+ txDonation ℕ.+ tot ℕ.+ (remDepTot ℕ.+ fees) + ≡t⟨⟩ + bal ℕ.+ (txFee ℕ.+ txDonation ℕ.+ (tot ℕ.+ remDepTot) ℕ.+ fees) + ≡⟨ cong (bal +_) $ begin + txFee + txDonation + (tot + remDepTot) + fees + ≡⟨ +-comm _ fees ⟩ + fees ℕ.+ (txFee ℕ.+ txDonation ℕ.+ (tot ℕ.+ remDepTot)) + ≡t⟨⟩ + (fees ℕ.+ txFee) ℕ.+ (txDonation ℕ.+ (tot ℕ.+ remDepTot)) + ≡⟨ cong ((fees + txFee) +_) $ +-comm txDonation (tot + remDepTot) ⟩ + (fees + txFee) ℕ.+ ((tot + remDepTot) ℕ.+ txDonation) + ≡t⟨⟩ + (fees + txFee) ℕ.+ (tot + remDepTot) ℕ.+ txDonation + ≡⟨ cong (λ x → (fees + txFee) + x + txDonation) + $ begin tot + (dep - ref) ≡˘⟨ +-∸-assoc tot ref≤dep ⟩ + (tot + dep) - ref ≡⟨ cong (_- ref) $ +-comm tot dep ⟩ + (dep + tot) - ref ≡˘⟨ deposits-change ⟩ + uDep ≡⟨ cong getCoin $ sym h ⟩ + getCoin deposits' ∎ ⟩ + (fees + txFee) + getCoin deposits' + txDonation + ∎ ⟩ + bal + ((fees + txFee) + getCoin deposits' + txDonation) + ∎ + + module _ (balanceUtxo balanceUtxo' : Coin) + (ref-prop : balanceUtxo + ref + wdls ≡ balanceUtxo' + txFee + txDonation + tot) + (h : deposits' ≡ updateDeposits pp txb deposits) + where + + pov-scripts-worker : isValid ≡ true + → balanceUtxo + fees + getCoin deposits + donations + wdls * χ(isValid) + ≡ balanceUtxo' + (fees + txFee) + getCoin deposits' + (donations + txDonation) + pov-scripts-worker valid = begin + balanceUtxo + fees + dep + donations + wdls * χ(isValid) + ≡⟨ cong (λ x → balanceUtxo + fees + dep + donations + wdls * χ x) valid ⟩ + balanceUtxo + fees + dep + donations + wdls * 1 + ≡⟨ cong (balanceUtxo + fees + dep + donations +_) (*-identityʳ wdls) ⟩ + balanceUtxo + fees + dep + donations + wdls + ≡⟨ +-assoc (balanceUtxo + fees + dep) donations wdls ⟩ + balanceUtxo + fees + dep + (donations + wdls) + ≡⟨ cong (balanceUtxo + fees + dep +_) (+-comm donations wdls) ⟩ + balanceUtxo + fees + dep + (wdls + donations) + ≡˘⟨ +-assoc (balanceUtxo + fees + dep) wdls donations ⟩ + balanceUtxo + fees + dep + wdls + donations + ≡⟨ cong (_+ donations) + $ begin + balanceUtxo + fees + dep + wdls + ≡˘⟨ cong (λ x → balanceUtxo + fees + x + wdls) (m+[n∸m]≡n ref≤dep) ⟩ + balanceUtxo + fees + (ref + remDepTot) + wdls + ≡⟨ cong (_+ wdls) (+-assoc balanceUtxo fees (ref + remDepTot)) ⟩ + balanceUtxo + (fees + (ref + remDepTot)) + wdls + ≡⟨ cong (λ x → balanceUtxo + x + wdls) (+-comm fees (ref + remDepTot)) ⟩ + balanceUtxo + (ref + remDepTot + fees) + wdls + ≡⟨ cong (λ x → balanceUtxo + x + wdls) (+-assoc ref remDepTot fees) ⟩ -- + balanceUtxo + (ref + (remDepTot + fees)) + wdls + ≡⟨ +-assoc balanceUtxo (ref + (remDepTot + fees)) wdls ⟩ -- + balanceUtxo + (ref + (remDepTot + fees) + wdls) + ≡⟨ cong (balanceUtxo +_) (+-assoc ref (remDepTot + fees) wdls) ⟩ + balanceUtxo + (ref + ((remDepTot + fees) + wdls)) + ≡⟨ cong (λ x → balanceUtxo + (ref + x)) (+-comm (remDepTot + fees) wdls) ⟩ + balanceUtxo + (ref + (wdls + (remDepTot + fees))) + ≡˘⟨ +-assoc balanceUtxo ref (wdls + (remDepTot + fees)) ⟩ + balanceUtxo + ref + (wdls + (remDepTot + fees)) + ≡˘⟨ +-assoc (balanceUtxo + ref) wdls (remDepTot + fees) ⟩ + balanceUtxo + ref + wdls + (remDepTot + fees) + ≡⟨ cong (_+ (remDepTot + fees)) ref-prop ⟩ + balanceUtxo' + txFee + txDonation + tot + (remDepTot + fees) + ≡⟨ rearrange0 (balanceUtxo') h ⟩ + balanceUtxo' + (fees + txFee + getCoin deposits' + txDonation) + ∎ ⟩ + balanceUtxo' ℕ.+ (fees + txFee ℕ.+ getCoin deposits' ℕ.+ txDonation) ℕ.+ donations + ≡t⟨⟩ + balanceUtxo' ℕ.+ (fees + txFee) ℕ.+ getCoin deposits' ℕ.+ (txDonation ℕ.+ donations) + ≡⟨ cong (balanceUtxo' + (fees + txFee) + getCoin deposits' ℕ.+_) + $ +-comm txDonation donations ⟩ + balanceUtxo' + (fees + txFee) + getCoin deposits' + (donations + txDonation) + ∎ + + pov-scripts : deposits' ≡ updateDeposits pp txb deposits + → isValid ≡ true + → cbalance utxo + fees + dep + donations + wdls * χ(isValid) + ≡ cbalance ((utxo ∣ txIns ᶜ) ∪ˡ outs txb) + + (fees + txFee) + getCoin deposits' + (donations + txDonation) + pov-scripts h valid = pov-scripts-worker (cbalance utxo) (cbalance ((utxo ∣ txIns ᶜ) ∪ˡ outs txb)) utxo-ref-prop h valid + + pov-no-scripts : isValid ≡ false + → cbalance utxo + fees + dep + donations + wdls * χ(isValid) + ≡ cbalance (utxo ∣ collateralInputs ᶜ) + (fees + cbalance (utxo ∣ collateralInputs)) + dep + donations + pov-no-scripts invalid = begin + cbalance utxo + fees + dep + donations + wdls * χ(isValid) ≡⟨ cong (λ x → cbalance utxo + fees + dep + donations + wdls * χ x) invalid ⟩ + cbalance utxo + fees + dep + donations + wdls * 0 ≡⟨ cong (cbalance utxo + fees + dep + donations +_ ) (*-zeroʳ wdls) ⟩ + cbalance utxo + fees + dep + donations + 0 ≡⟨ +-identityʳ _ ⟩ + cbalance utxo + fees + dep + donations ≡⟨ cong (λ x → x + dep + donations) $ begin + cbalance utxo ℕ.+ fees ≡⟨ cong (_+ fees) (split-balance collateralInputs) ⟩ + cbalance (utxo ∣ collateralInputs ᶜ) ℕ.+ cbalance (utxo ∣ collateralInputs) ℕ.+ fees ≡t⟨⟩ + cbalance (utxo ∣ collateralInputs ᶜ) ℕ.+ (cbalance (utxo ∣ collateralInputs) ℕ.+ fees) ≡⟨ cong (cbalance (utxo ∣ collateralInputs ᶜ) +_) (+-comm _ fees) ⟩ + cbalance (utxo ∣ collateralInputs ᶜ) ℕ.+ (fees ℕ.+ cbalance (utxo ∣ collateralInputs)) ∎ ⟩ + cbalance (utxo ∣ collateralInputs ᶜ) + (fees + cbalance (utxo ∣ collateralInputs)) + dep + donations + ∎ diff --git a/src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md b/src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md new file mode 100644 index 000000000..0f08b70be --- /dev/null +++ b/src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md @@ -0,0 +1,192 @@ + + +## General Minimum Spending Condition + +```agda +isRefundCert : DCert → Bool +isRefundCert (dereg c _) = true +isRefundCert (deregdrep c _) = true +isRefundCert _ = false + +noRefundCert : List DCert → Type _ +noRefundCert l = All (λ cert → isRefundCert cert ≡ false) l + +opaque + unfolding List-Model + unfolding finiteness + fin∘list[] : {A : Type} → proj₁ (finiteness{A = A} ∅) ≡ [] + fin∘list[] = refl + fin∘list∷[] : {A : Type} {a : A} → proj₁ (finiteness ❴ a ❵) ≡ [ a ] + fin∘list∷[] = refl + +coin∅ : getCoin{A = Deposits} ∅ ≡ 0 +coin∅ = begin + foldr (λ x → (proj₂ x) +_) 0 (deduplicate _≟_ (proj₁ (finiteness ∅))) + ≡⟨ cong (λ u → (foldr (λ x → (proj₂ x) +_) 0 (deduplicate _≟_ u))) fin∘list[] ⟩ + foldr (λ (x : DepositPurpose × Coin) → (proj₂ x) +_) 0 (deduplicate _≟_ []) + ≡⟨ cong (λ u → (foldr (λ (x : DepositPurpose × Coin) → (proj₂ x) +_) 0 u)) + {x = deduplicate _≟_ []} {y = []} refl ⟩ + foldr (λ (x : DepositPurpose × Coin) → (proj₂ x) +_) 0 [] + ≡⟨ refl ⟩ + 0 ∎ + where open Prelude.≡-Reasoning + +getCoin-singleton : ((dp , c) : DepositPurpose × Coin) → indexedSumᵛ' id ❴ (dp , c) ❵ ≡ c +getCoin-singleton _ = indexedSum-singleton' {A = DepositPurpose × Coin} {f = proj₂} (finiteness _) + +module _ -- ASSUMPTION -- + (gc-hom : (d₁ d₂ : Deposits) → getCoin (d₁ ∪⁺ d₂) ≡ getCoin d₁ + getCoin d₂) + where + ∪⁺singleton≡ : {deps : Deposits} {(dp , c) : DepositPurpose × Coin} + → getCoin (deps ∪⁺ ❴ (dp , c) ❵ᵐ) ≡ getCoin deps + c + ∪⁺singleton≡ {deps} {(dp , c)} = begin + getCoin (deps ∪⁺ ❴ (dp , c) ❵) + ≡⟨ gc-hom deps ❴ (dp , c) ❵ ⟩ + getCoin deps + getCoin{A = Deposits} ❴ (dp , c) ❵ + ≡⟨ cong (getCoin deps +_) (getCoin-singleton (dp , c)) ⟩ + getCoin deps + c + ∎ + where open Prelude.≡-Reasoning + + module _ {deposits : Deposits} {txid : TxId} {gaDep : Coin} where + + ≤updatePropDeps : (props : List GovProposal) + → getCoin deposits ≤ getCoin (updateProposalDeposits props txid gaDep deposits) + ≤updatePropDeps [] = ≤-reflexive refl + ≤updatePropDeps (x ∷ props) = ≤-trans (≤updatePropDeps props) + (≤-trans (m≤m+n _ _) + (≤-reflexive $ sym $ ∪⁺singleton≡)) + updatePropDeps≡ : (ps : List GovProposal) + → getCoin (updateProposalDeposits ps txid gaDep deposits) - getCoin deposits ≡ (length ps) * gaDep + updatePropDeps≡ [] = n∸n≡0 (getCoin deposits) + updatePropDeps≡ (_ ∷ ps) = let + upD = updateProposalDeposits ps txid gaDep deposits in + begin + getCoin (upD ∪⁺ ❴ GovActionDeposit (txid , length ps) , gaDep ❵ᵐ) ∸ getCoin deposits + ≡⟨ cong (_∸ getCoin deposits) ∪⁺singleton≡ ⟩ + getCoin upD + gaDep ∸ getCoin deposits + ≡⟨ +-∸-comm _ (≤updatePropDeps ps) ⟩ + (getCoin upD ∸ getCoin deposits) + gaDep + ≡⟨ cong (_+ gaDep) (updatePropDeps≡ ps) ⟩ + (length ps) * gaDep + gaDep + ≡⟨ +-comm ((length ps) * gaDep) gaDep ⟩ + gaDep + (length ps) * gaDep + ∎ + where open Prelude.≡-Reasoning + + ≤certDeps : {d : Deposits} {(dp , c) : DepositPurpose × Coin} + → getCoin d ≤ getCoin (d ∪⁺ ❴ (dp , c) ❵) + + ≤certDeps {d} = begin + getCoin d ≤⟨ m≤m+n (getCoin d) _ ⟩ + getCoin d + _ ≡⟨ sym ∪⁺singleton≡ ⟩ + getCoin (d ∪⁺ ❴ _ ❵) ∎ + where open ≤-Reasoning + + + ≤updateCertDeps : (cs : List DCert) {pp : PParams} {deposits : Deposits} + → noRefundCert cs + → getCoin deposits ≤ getCoin (updateCertDeposits pp cs deposits) + ≤updateCertDeps [] nrf = ≤-reflexive refl + ≤updateCertDeps (reg c v ∷ cs) {pp} {deposits} (_ All.∷ nrf) = + ≤-trans ≤certDeps (≤updateCertDeps cs {pp} {deposits ∪⁺ ❴ CredentialDeposit c , pp .PParams.keyDeposit ❵} nrf) + ≤updateCertDeps (delegate c _ _ v ∷ cs) {pp} {deposits} (_ All.∷ nrf) = + ≤-trans ≤certDeps (≤updateCertDeps cs {pp} {deposits ∪⁺ ❴ CredentialDeposit c , v ❵} nrf) + ≤updateCertDeps (regpool _ _ ∷ cs) (_ All.∷ nrf) = ≤-trans ≤certDeps (≤updateCertDeps cs nrf) + ≤updateCertDeps (retirepool _ _ ∷ cs) (_ All.∷ nrf) = ≤updateCertDeps cs nrf + ≤updateCertDeps (regdrep _ _ _ ∷ cs) (_ All.∷ nrf) = ≤-trans ≤certDeps (≤updateCertDeps cs nrf) + ≤updateCertDeps (ccreghot _ _ ∷ cs) (_ All.∷ nrf) = ≤updateCertDeps cs nrf +``` + +### Main Theorem: General Minimum Spending Condition + + + +```agda + gmsc : let open Tx tx renaming (body to txb); open TxBody txb + pp = UTxOEnv.pparams Γ; open PParams pp + open UTxOState utxoState + renaming (utxo to st; fees to fs; deposits to deps; donations to dons) + in + Γ ⊢ ⟦ st , fs , deps , dons ⟧ ⇀⦇ tx ,UTXO⦈ + ⟦ utxo' , fees' , deposits' , donations' ⟧ + + → noRefundCert txCerts -- FINAL ASSUMPTION -- + + ------------------------------------------------------------------- + → coin (consumed pp utxoState txb) ≥ length txGovProposals * govActionDeposit + + gmsc step@(UTXO-inductive⋯ tx Γ utxoState _ _ _ _ _ _ c≡p cmint≡0 _ _ _ _ _ _ _ _ _ _) nrf = + begin + length txGovProposals * govActionDeposit + ≡˘⟨ updatePropDeps≡ txGovProposals ⟩ + getCoin (updateProposalDeposits txGovProposals txId govActionDeposit deps) ∸ getCoin deps + ≤⟨ ∸-monoˡ-≤ (getCoin deps) (≤updateCertDeps txCerts nrf) ⟩ + getCoin (updateDeposits pp txb deps) - getCoin deps + ≡⟨ ∸≡posPart⊖ {getCoin (updateDeposits pp txb deps)} {getCoin deps} ⟩ + newDeps + ≤⟨ m≤n+m newDeps (coin balOut + txFee + txDonation) ⟩ + coin balOut + txFee + txDonation + newDeps + ≡⟨ +-assoc (coin balOut + txFee) txDonation newDeps ⟩ + coin balOut + txFee + (txDonation + newDeps) + ≡⟨ cong (coin balOut + txFee +_) (+-comm txDonation newDeps) ⟩ + coin balOut + txFee + (newDeps + txDonation) + ≡˘⟨ +-assoc (coin balOut + txFee) newDeps txDonation ⟩ + coin balOut + txFee + newDeps + txDonation + ≡˘⟨ cong (λ x → x + newDeps + txDonation) coin-inject-lemma ⟩ + coin (balOut + inject txFee) + newDeps + txDonation + ≡˘⟨ cong (_+ txDonation) coin-inject-lemma ⟩ + coin (balOut + inject txFee + inject newDeps) + txDonation + ≡˘⟨ coin-inject-lemma ⟩ + coin (balOut + inject txFee + inject newDeps + inject txDonation) + ≡˘⟨ cong coin c≡p ⟩ + coin (balIn + mint + inject refunds + inject wdrls) ∎ + where + open ≤-Reasoning + pp : PParams + pp = UTxOEnv.pparams Γ; open PParams pp + open Tx tx renaming (body to txb); open TxBody txb + open UTxOState utxoState renaming (utxo to st; fees to fs; deposits to deps; donations to dons) + + newDeps refunds wdrls : Coin + newDeps = newDeposits pp utxoState txb + refunds = depositRefunds pp utxoState txb + wdrls = getCoin txWithdrawals + + balIn balOut : Value + balIn = balance (st ∣ txIns) + balOut = balance (outs txb) +``` + + diff --git a/src/Ledger/Conway/Specification/Utxo/Properties/MinSpend.lagda.md b/src/Ledger/Conway/Specification/Utxo/Properties/MinSpend.lagda.md index ce49c5947..bfa8eb386 100644 --- a/src/Ledger/Conway/Specification/Utxo/Properties/MinSpend.lagda.md +++ b/src/Ledger/Conway/Specification/Utxo/Properties/MinSpend.lagda.md @@ -19,104 +19,14 @@ open import Ledger.Conway.Specification.Ledger txs abs open import Ledger.Prelude hiding (≤-trans; ≤-antisym; All) open import Ledger.Conway.Specification.Properties txs abs using (validTxIn₂) open import Ledger.Conway.Specification.Utxo txs abs +open import Ledger.Conway.Specification.Utxo.Properties.GenMinSpend txs abs open import Data.List.Relation.Unary.All using (All) open import Data.Nat.Properties hiding (_≟_) -isRefundCert : DCert → Bool -isRefundCert (dereg c _) = true -isRefundCert (deregdrep c _) = true -isRefundCert _ = false - -noRefundCert : List DCert → Type _ -noRefundCert l = All (λ cert → isRefundCert cert ≡ false) l - -opaque - unfolding List-Model - unfolding finiteness - fin∘list[] : {A : Type} → proj₁ (finiteness{A = A} ∅) ≡ [] - fin∘list[] = refl - fin∘list∷[] : {A : Type} {a : A} → proj₁ (finiteness ❴ a ❵) ≡ [ a ] - fin∘list∷[] = refl - -coin∅ : getCoin{A = DepositPurpose ⇀ Coin} ∅ ≡ 0 -coin∅ = begin - foldr (λ x → (proj₂ x) +_) 0 (deduplicate _≟_ (proj₁ (finiteness ∅))) - ≡⟨ cong (λ u → (foldr (λ x → (proj₂ x) +_) 0 (deduplicate _≟_ u))) fin∘list[] ⟩ - foldr (λ (x : DepositPurpose × Coin) → (proj₂ x) +_) 0 (deduplicate _≟_ []) - ≡⟨ cong (λ u → (foldr (λ (x : DepositPurpose × Coin) → (proj₂ x) +_) 0 u)) - {x = deduplicate _≟_ []} {y = []} refl ⟩ - foldr (λ (x : DepositPurpose × Coin) → (proj₂ x) +_) 0 [] - ≡⟨ refl ⟩ - 0 ∎ - where open ≡-Reasoning - -getCoin-singleton : ((dp , c) : DepositPurpose × Coin) → indexedSumᵛ' id ❴ (dp , c) ❵ ≡ c -getCoin-singleton _ = indexedSum-singleton' {A = DepositPurpose × Coin} {f = proj₂} (finiteness _) - -module _ -- ASSUMPTION -- - (gc-hom : (d₁ d₂ : DepositPurpose ⇀ Coin) → getCoin (d₁ ∪⁺ d₂) ≡ getCoin d₁ + getCoin d₂) +module _ where - ∪⁺singleton≡ : {deps : DepositPurpose ⇀ Coin} {(dp , c) : DepositPurpose × Coin} - → getCoin (deps ∪⁺ ❴ (dp , c) ❵ᵐ) ≡ getCoin deps + c - ∪⁺singleton≡ {deps} {(dp , c)} = begin - getCoin (deps ∪⁺ ❴ (dp , c) ❵) - ≡⟨ gc-hom deps ❴ (dp , c) ❵ ⟩ - getCoin deps + getCoin{A = DepositPurpose ⇀ Coin} ❴ (dp , c) ❵ - ≡⟨ cong (getCoin deps +_) (getCoin-singleton (dp , c)) ⟩ - getCoin deps + c - ∎ - where open ≡-Reasoning - - module _ {deposits : DepositPurpose ⇀ Coin} {txid : TxId} {gaDep : Coin} where - - ≤updatePropDeps : (props : List GovProposal) - → getCoin deposits ≤ getCoin (updateProposalDeposits props txid gaDep deposits) - ≤updatePropDeps [] = ≤-reflexive refl - ≤updatePropDeps (x ∷ props) = ≤-trans (≤updatePropDeps props) - (≤-trans (m≤m+n _ _) - (≤-reflexive $ sym $ ∪⁺singleton≡)) - updatePropDeps≡ : (ps : List GovProposal) - → getCoin (updateProposalDeposits ps txid gaDep deposits) - getCoin deposits ≡ (length ps) * gaDep - updatePropDeps≡ [] = n∸n≡0 (getCoin deposits) - updatePropDeps≡ (_ ∷ ps) = let - upD = updateProposalDeposits ps txid gaDep deposits in - begin - getCoin (upD ∪⁺ ❴ GovActionDeposit (txid , length ps) , gaDep ❵ᵐ) ∸ getCoin deposits - ≡⟨ cong (_∸ getCoin deposits) ∪⁺singleton≡ ⟩ - getCoin upD + gaDep ∸ getCoin deposits - ≡⟨ +-∸-comm _ (≤updatePropDeps ps) ⟩ - (getCoin upD ∸ getCoin deposits) + gaDep - ≡⟨ cong (_+ gaDep) (updatePropDeps≡ ps) ⟩ - (length ps) * gaDep + gaDep - ≡⟨ +-comm ((length ps) * gaDep) gaDep ⟩ - gaDep + (length ps) * gaDep - ∎ - where open ≡-Reasoning - - ≤certDeps : {d : DepositPurpose ⇀ Coin} {(dp , c) : DepositPurpose × Coin} - → getCoin d ≤ getCoin (d ∪⁺ ❴ (dp , c) ❵) - - ≤certDeps {d} = begin - getCoin d ≤⟨ m≤m+n (getCoin d) _ ⟩ - getCoin d + _ ≡⟨ sym ∪⁺singleton≡ ⟩ - getCoin (d ∪⁺ ❴ _ ❵) ∎ - where open ≤-Reasoning - - - ≤updateCertDeps : (cs : List DCert) {pp : PParams} {deposits : DepositPurpose ⇀ Coin} - → noRefundCert cs - → getCoin deposits ≤ getCoin (updateCertDeposits pp cs deposits) - ≤updateCertDeps [] nrf = ≤-reflexive refl - ≤updateCertDeps (reg c v ∷ cs) {pp} {deposits} (_ All.∷ nrf) = - ≤-trans ≤certDeps (≤updateCertDeps cs {pp} {deposits ∪⁺ ❴ CredentialDeposit c , pp .PParams.keyDeposit ❵} nrf) - ≤updateCertDeps (delegate c _ _ v ∷ cs) {pp} {deposits} (_ All.∷ nrf) = - ≤-trans ≤certDeps (≤updateCertDeps cs {pp} {deposits ∪⁺ ❴ CredentialDeposit c , v ❵} nrf) - ≤updateCertDeps (regpool _ _ ∷ cs) (_ All.∷ nrf) = ≤-trans ≤certDeps (≤updateCertDeps cs nrf) - ≤updateCertDeps (retirepool _ _ ∷ cs) (_ All.∷ nrf) = ≤updateCertDeps cs nrf - ≤updateCertDeps (regdrep _ _ _ ∷ cs) (_ All.∷ nrf) = ≤-trans ≤certDeps (≤updateCertDeps cs nrf) - ≤updateCertDeps (ccreghot _ _ ∷ cs) (_ All.∷ nrf) = ≤updateCertDeps cs nrf ``` --> @@ -140,16 +50,16 @@ proposals in `tx`{.AgdaBound}. *Formally*. - -```agda utxoMinSpend : {tx : Tx} {s s' : UTxOState} → Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s' → noRefundCert (DCertsOf tx) @@ -162,9 +72,9 @@ proposals in `tx`{.AgdaBound}. utxoMinSpend step@(UTXO-inductive⋯ tx Γ utxoSt _ _ _ _ _ _ c≡p cmint≡0 _ _ _ _ _ _ _ _ _ _) nrf = begin length txGovProposals * govActionDeps - ≡˘⟨ updatePropDeps≡ txGovProposals ⟩ + ≡˘⟨ updatePropDeps≡ gc-hom txGovProposals ⟩ getCoin (updateProposalDeposits txGovProposals txId (govActionDeps) deposits) ∸ getCoin deposits - ≤⟨ ∸-monoˡ-≤ (getCoin deposits) (≤updateCertDeps txCerts nrf) ⟩ + ≤⟨ ∸-monoˡ-≤ (getCoin deposits) (≤updateCertDeps gc-hom txCerts nrf) ⟩ getCoin (updateDeposits (PParamsOf Γ) txb deposits) - getCoin deposits ≡⟨ ∸≡posPart⊖ {getCoin (updateDeposits (PParamsOf Γ) txb deposits)} {getCoin deposits} ⟩ newDeps diff --git a/src/Ledger/Conway/Specification/Utxo/Properties/PoV.lagda.md b/src/Ledger/Conway/Specification/Utxo/Properties/PoV.lagda.md index 1fd7207c5..775064f8a 100644 --- a/src/Ledger/Conway/Specification/Utxo/Properties/PoV.lagda.md +++ b/src/Ledger/Conway/Specification/Utxo/Properties/PoV.lagda.md @@ -14,7 +14,7 @@ module Ledger.Conway.Specification.Utxo.Properties.PoV open import Ledger.Conway.Specification.Certs govStructure open import Ledger.Prelude open import Ledger.Conway.Specification.Utxo txs abs -open import Ledger.Conway.Specification.Utxo.Properties txs abs using (χ; module DepositHelpers) +open import Ledger.Conway.Specification.Utxo.Properties.DepositHelpers txs abs public open UTxOState; open Tx; open TxBody ``` --> @@ -58,8 +58,8 @@ UTXOpov : {Γ : UTxOEnv} {tx : Tx} {s s' : UTxOState} ```agda UTXOpov h' step@(UTXO-inductive⋯ _ Γ _ _ _ _ _ _ _ newBal noMintAda _ _ _ _ _ _ _ _ _ (Scripts-Yes (_ , _ , valid))) - = DepositHelpers.pov-scripts step h' refl valid + = pov-scripts step h' refl valid UTXOpov h' step@(UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (Scripts-No (_ , invalid))) - = DepositHelpers.pov-no-scripts step h' invalid + = pov-no-scripts step h' invalid ``` From 3e3033bbac18823d7631fd777647fd2b51e63116 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Thu, 25 Sep 2025 16:39:01 -0600 Subject: [PATCH 2/6] major reorganization of Properties modules --- .../Conway/Conformance/Ledger/Properties.agda | 2 +- src/Ledger/Conway/Foreign/HSLedger/Gov.agda | 2 +- .../BlockBody/Properties.lagda.md | 2 +- .../Specification/Certs/Properties.agda | 165 +---------------- .../Certs/Properties/Computational.agda | 163 +++++++++++++++++ .../Specification/Chain/Properties.agda | 51 +----- .../Chain/Properties/Computational.agda | 47 +++++ .../Chain/Properties/GovDepsMatch.lagda.md | 2 +- .../Specification/Epoch/Properties.agda | 170 +---------------- .../Epoch/Properties/Computational.agda | 168 +++++++++++++++++ .../Epoch/Properties/GovDepsMatch.lagda.md | 2 +- .../Conway/Specification/Gov/Properties.agda | 171 +----------------- .../Gov/Properties/Computational.agda | 171 ++++++++++++++++++ .../Specification/Ledger/Properties.agda | 8 + .../Ledger/Properties/Computational.lagda | 77 ++++++++ .../Ledger/Properties/GovDepsMatch.lagda.md | 3 +- .../Setoid.lagda} | 72 +------- .../RewardUpdate/Properties.lagda.md | 2 +- .../Test/Examples/HelloWorld.agda | 2 +- .../Test/Examples/SucceedIfNumber.agda | 2 +- .../Conway/Specification/Utxo/Properties.agda | 9 + .../Computational.lagda} | 2 +- .../Specification/Utxow/Properties.agda | 2 +- 23 files changed, 679 insertions(+), 616 deletions(-) create mode 100644 src/Ledger/Conway/Specification/Certs/Properties/Computational.agda create mode 100644 src/Ledger/Conway/Specification/Chain/Properties/Computational.agda create mode 100644 src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda create mode 100644 src/Ledger/Conway/Specification/Gov/Properties/Computational.agda create mode 100644 src/Ledger/Conway/Specification/Ledger/Properties.agda create mode 100644 src/Ledger/Conway/Specification/Ledger/Properties/Computational.lagda rename src/Ledger/Conway/Specification/Ledger/{Properties.lagda => Properties/Setoid.lagda} (88%) create mode 100644 src/Ledger/Conway/Specification/Utxo/Properties.agda rename src/Ledger/Conway/Specification/Utxo/{Properties.lagda => Properties/Computational.lagda} (99%) diff --git a/src/Ledger/Conway/Conformance/Ledger/Properties.agda b/src/Ledger/Conway/Conformance/Ledger/Properties.agda index afc9d6712..8aa064929 100644 --- a/src/Ledger/Conway/Conformance/Ledger/Properties.agda +++ b/src/Ledger/Conway/Conformance/Ledger/Properties.agda @@ -16,7 +16,7 @@ open import Ledger.Conway.Specification.Enact govStructure open import Ledger.Conway.Conformance.Epoch txs abs open import Ledger.Conway.Conformance.Certs.Properties govStructure open import Ledger.Conway.Specification.Gov txs -open import Ledger.Conway.Specification.Gov.Properties txs +open import Ledger.Conway.Specification.Gov.Properties.Computational txs open import Ledger.Conway.Conformance.Ledger txs abs open import Ledger.Conway.Specification.Ratify txs hiding (vote) open import Ledger.Conway.Conformance.Utxo txs abs diff --git a/src/Ledger/Conway/Foreign/HSLedger/Gov.agda b/src/Ledger/Conway/Foreign/HSLedger/Gov.agda index 4603998d8..07b28db7d 100644 --- a/src/Ledger/Conway/Foreign/HSLedger/Gov.agda +++ b/src/Ledger/Conway/Foreign/HSLedger/Gov.agda @@ -14,7 +14,7 @@ open import Ledger.Conway.Conformance.Certs govStructure open import Ledger.Conway.Specification.Enact govStructure open import Ledger.Conway.Conformance.Gov it it import Ledger.Conway.Specification.Gov it as L -open import Ledger.Conway.Specification.Gov.Properties it +open import Ledger.Conway.Specification.Gov.Properties.Computational it instance diff --git a/src/Ledger/Conway/Specification/BlockBody/Properties.lagda.md b/src/Ledger/Conway/Specification/BlockBody/Properties.lagda.md index dc1d812c3..0342ef786 100644 --- a/src/Ledger/Conway/Specification/BlockBody/Properties.lagda.md +++ b/src/Ledger/Conway/Specification/BlockBody/Properties.lagda.md @@ -9,7 +9,7 @@ module Ledger.Conway.Specification.BlockBody.Properties (abs : AbstractFunctions txs) (open AbstractFunctions abs) where open import Ledger.Conway.Specification.BlockBody txs abs -open import Ledger.Conway.Specification.Ledger.Properties txs abs +open import Ledger.Conway.Specification.Ledger.Properties.Computational txs abs open import Ledger.Prelude open Computational ⦃...⦄ diff --git a/src/Ledger/Conway/Specification/Certs/Properties.agda b/src/Ledger/Conway/Specification/Certs/Properties.agda index 0bfa66a5c..dc820eca6 100644 --- a/src/Ledger/Conway/Specification/Certs/Properties.agda +++ b/src/Ledger/Conway/Specification/Certs/Properties.agda @@ -1,163 +1,8 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude -open import Ledger.Conway.Specification.Gov.Base +module Ledger.Conway.Specification.Certs.Properties where -module Ledger.Conway.Specification.Certs.Properties (gs : _) (open GovStructure gs) where - -open import Data.Maybe.Properties -open import Relation.Nullary.Decidable - -open import Tactic.ReduceDec - -open import Algebra using (CommutativeMonoid) -open import Ledger.Conway.Specification.Gov.Actions gs hiding (yes; no) -open import Ledger.Conway.Specification.Certs gs - -open import Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid; +-identityʳ; +-identityˡ) -open import Axiom.Set.Properties th -open import Relation.Binary using (IsEquivalence) -open Computational ⦃...⦄ - -open import stdlib-meta.Tactic.GenError using (genErrors) - -open CertState -open GovVote using (voter) - -instance - Computational-DELEG : Computational _⊢_⇀⦇_,DELEG⦈_ String - Computational-DELEG .computeProof de stᵈ = - let open DelegEnv de; open DState stᵈ in - λ where - (delegate c mv mc d) → case ¿ (c ∉ dom rewards → d ≡ pparams .PParams.keyDeposit) - × (c ∈ dom rewards → d ≡ 0) - × mv ∈ mapˢ (just ∘ vDelegCredential) delegatees ∪ - fromList ( nothing ∷ just vDelegAbstain ∷ just vDelegNoConfidence ∷ [] ) - × mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵ - ¿ of λ where - (yes p) → success (-, DELEG-delegate p) - (no ¬p) → failure (genErrors ¬p) - (dereg c d) → case ¿ (c , 0) ∈ rewards ¿ of λ where - (yes p) → success (-, DELEG-dereg p) - (no ¬p) → failure (genErrors ¬p) - (reg c d) → case ¿ c ∉ dom rewards - × (d ≡ pparams .PParams.keyDeposit ⊎ d ≡ 0) - ¿ of λ where - (yes p) → success (-, DELEG-reg p) - (no ¬p) → failure (genErrors ¬p) - _ → failure "Unexpected certificate in DELEG" - Computational-DELEG .completeness de stᵈ (delegate c mv mc d) - s' (DELEG-delegate p) rewrite dec-yes (¿ (c ∉ dom (DState.rewards stᵈ) → d ≡ DelegEnv.pparams de .PParams.keyDeposit) - × (c ∈ dom (DState.rewards stᵈ) → d ≡ 0) - × mv ∈ mapˢ (just ∘ vDelegCredential) (DelegEnv.delegatees de) ∪ fromList ( nothing ∷ just vDelegAbstain ∷ just vDelegNoConfidence ∷ [] ) - × mc ∈ mapˢ just (dom (DelegEnv.pools de)) ∪ ❴ nothing ❵ - ¿) p .proj₂ = refl - Computational-DELEG .completeness de stᵈ (dereg c d) _ (DELEG-dereg p) - rewrite dec-yes (¿ (c , 0) ∈ (DState.rewards stᵈ) ¿) p .proj₂ = refl - Computational-DELEG .completeness de stᵈ (reg c d) _ (DELEG-reg p) - rewrite dec-yes (¿ c ∉ dom (DState.rewards stᵈ) × (d ≡ DelegEnv.pparams de .PParams.keyDeposit ⊎ d ≡ 0) ¿) p .proj₂ = refl - - Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String - Computational-POOL .computeProof _ stᵖ (regpool c _) = - let open PState stᵖ in - case ¬? (c ∈? dom pools) of λ where - (yes p) → success (-, POOL-regpool p) - (no ¬p) → failure (genErrors ¬p) - Computational-POOL .computeProof _ _ (retirepool c e) = success (-, POOL-retirepool) - Computational-POOL .computeProof _ _ _ = failure "Unexpected certificate in POOL" - Computational-POOL .completeness _ stᵖ (regpool c _) _ (POOL-regpool ¬p) - rewrite dec-no (c ∈? dom (PState.pools stᵖ)) ¬p = refl - Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl - - Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_ String - Computational-GOVCERT .computeProof ce stᵍ (regdrep c d _) = - let open CertEnv ce; open PParams pp in - case ¿ (d ≡ drepDeposit × c ∉ dom (GState.dreps stᵍ)) - ⊎ (d ≡ 0 × c ∈ dom (GState.dreps stᵍ)) ¿ of λ where - (yes p) → success (-, GOVCERT-regdrep p) - (no ¬p) → failure (genErrors ¬p) - Computational-GOVCERT .computeProof _ stᵍ (deregdrep c _) = - let open GState stᵍ in - case c ∈? dom dreps of λ where - (yes p) → success (-, GOVCERT-deregdrep p) - (no ¬p) → failure (genErrors ¬p) - Computational-GOVCERT .computeProof ce stᵍ (ccreghot c _) = - let open CertEnv ce; open GState stᵍ in - case ¿ ((c , nothing) ∉ ccHotKeys ˢ) × c ∈ coldCreds ¿ of λ where - (yes p) → success (-, GOVCERT-ccreghot p) - (no ¬p) → failure (genErrors ¬p) - Computational-GOVCERT .computeProof _ _ _ = failure "Unexpected certificate in GOVCERT" - Computational-GOVCERT .completeness ce stᵍ - (regdrep c d _) _ (GOVCERT-regdrep p) - rewrite dec-yes - ¿ (let open CertEnv ce; open PParams pp; open GState stᵍ in - (d ≡ drepDeposit × c ∉ dom dreps) ⊎ (d ≡ 0 × c ∈ dom dreps)) - ¿ p .proj₂ = refl - Computational-GOVCERT .completeness _ stᵍ - (deregdrep c _) _ (GOVCERT-deregdrep p) - rewrite dec-yes (c ∈? dom (GState.dreps stᵍ)) p .proj₂ = refl - Computational-GOVCERT .completeness ce stᵍ - (ccreghot c _) _ (GOVCERT-ccreghot p) - rewrite dec-yes (¿ (((c , nothing) ∉ (GState.ccHotKeys stᵍ) ˢ) × c ∈ CertEnv.coldCreds ce) ¿) p .proj₂ = refl - - Computational-CERT : Computational _⊢_⇀⦇_,CERT⦈_ String - Computational-CERT .computeProof ce cs dCert - with computeProof ⟦ CertEnv.pp ce , PState.pools (pState cs) , dom (GState.dreps (gState cs)) ⟧ (dState cs) dCert - | computeProof (CertEnv.pp ce) (pState cs) dCert | computeProof ce (gState cs) dCert - ... | success (_ , h) | _ | _ = success (-, CERT-deleg h) - ... | failure _ | success (_ , h) | _ = success (-, CERT-pool h) - ... | failure _ | failure _ | success (_ , h) = success (-, CERT-vdel h) - ... | failure e₁ | failure e₂ | failure e₃ = failure $ - "DELEG: " <> e₁ <> "\nPOOL: " <> e₂ <> "\nVDEL: " <> e₃ - Computational-CERT .completeness ce cs - dCert@(delegate c mv mc d) cs' (CERT-deleg h) - with computeProof ⟦ CertEnv.pp ce , PState.pools (pState cs) , dom (GState.dreps (gState cs)) ⟧ (dState cs) dCert | completeness _ _ _ _ h - ... | success _ | refl = refl - Computational-CERT .completeness ce cs - dCert@(reg c d) cs' (CERT-deleg h) - with computeProof ⟦ CertEnv.pp ce , PState.pools (pState cs) , dom (GState.dreps (gState cs)) ⟧ (dState cs) dCert | completeness _ _ _ _ h - ... | success _ | refl = refl - Computational-CERT .completeness ce cs - dCert@(dereg c _) cs' (CERT-deleg h) - with computeProof ⟦ CertEnv.pp ce , PState.pools (pState cs) , dom (GState.dreps (gState cs)) ⟧ (dState cs) dCert | completeness _ _ _ _ h - ... | success _ | refl = refl - Computational-CERT .completeness ce cs - dCert@(regpool c poolParams) cs' (CERT-pool h) - with computeProof (CertEnv.pp ce) (pState cs) dCert | completeness _ _ _ _ h - ... | success _ | refl = refl - Computational-CERT .completeness ce cs - dCert@(retirepool c e) cs' (CERT-pool h) - with completeness _ _ _ _ h - ... | refl = refl - Computational-CERT .completeness ce cs - dCert@(regdrep c d an) - cs' (CERT-vdel h) - with computeProof ce (gState cs) dCert | completeness _ _ _ _ h - ... | success _ | refl = refl - Computational-CERT .completeness ce cs - dCert@(deregdrep c _) cs' (CERT-vdel h) - with computeProof ce (gState cs) dCert | completeness _ _ _ _ h - ... | success _ | refl = refl - Computational-CERT .completeness ce cs - dCert@(ccreghot c mkh) cs' (CERT-vdel h) - with computeProof ce (gState cs) dCert | completeness _ _ _ _ h - ... | success _ | refl = refl - - Computational-CERTBASE : Computational _⊢_⇀⦇_,CERTBASE⦈_ String - Computational-CERTBASE .computeProof ce cs _ = - let open CertEnv ce; open PParams pp - open GState (gState cs); open DState (dState cs) - refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList votes) - refreshedDReps = mapValueRestricted (const (CertEnv.epoch ce + drepActivity)) dreps refresh - in case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs - × mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where - (yes p) → success (-, CERT-base p) - (no ¬p) → failure (genErrors ¬p) - Computational-CERTBASE .completeness ce st _ st' (CERT-base p) - rewrite let dState = CertState.dState st; open DState dState in - dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom (CertEnv.wdrls ce))) ⊆ dom voteDelegs - × mapˢ (map₁ RwdAddr.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿ - p .proj₂ = refl - -Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String -Computational-CERTS = it +open import Ledger.Conway.Specification.Certs.Properties.Computational +open import Ledger.Conway.Specification.Certs.Properties.PoV +open import Ledger.Conway.Specification.Certs.Properties.PoVLemmas +open import Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg diff --git a/src/Ledger/Conway/Specification/Certs/Properties/Computational.agda b/src/Ledger/Conway/Specification/Certs/Properties/Computational.agda new file mode 100644 index 000000000..1442760cc --- /dev/null +++ b/src/Ledger/Conway/Specification/Certs/Properties/Computational.agda @@ -0,0 +1,163 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Gov.Base + +module Ledger.Conway.Specification.Certs.Properties.Computational (gs : _) (open GovStructure gs) where + +open import Data.Maybe.Properties +open import Relation.Nullary.Decidable + +open import Tactic.ReduceDec + +open import Algebra using (CommutativeMonoid) +open import Ledger.Conway.Specification.Gov.Actions gs hiding (yes; no) +open import Ledger.Conway.Specification.Certs gs + +open import Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid; +-identityʳ; +-identityˡ) +open import Axiom.Set.Properties th +open import Relation.Binary using (IsEquivalence) +open Computational ⦃...⦄ + +open import stdlib-meta.Tactic.GenError using (genErrors) + +open CertState +open GovVote using (voter) + +instance + Computational-DELEG : Computational _⊢_⇀⦇_,DELEG⦈_ String + Computational-DELEG .computeProof de stᵈ = + let open DelegEnv de; open DState stᵈ in + λ where + (delegate c mv mc d) → case ¿ (c ∉ dom rewards → d ≡ pparams .PParams.keyDeposit) + × (c ∈ dom rewards → d ≡ 0) + × mv ∈ mapˢ (just ∘ vDelegCredential) delegatees ∪ + fromList ( nothing ∷ just vDelegAbstain ∷ just vDelegNoConfidence ∷ [] ) + × mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵ + ¿ of λ where + (yes p) → success (-, DELEG-delegate p) + (no ¬p) → failure (genErrors ¬p) + (dereg c d) → case ¿ (c , 0) ∈ rewards ¿ of λ where + (yes p) → success (-, DELEG-dereg p) + (no ¬p) → failure (genErrors ¬p) + (reg c d) → case ¿ c ∉ dom rewards + × (d ≡ pparams .PParams.keyDeposit ⊎ d ≡ 0) + ¿ of λ where + (yes p) → success (-, DELEG-reg p) + (no ¬p) → failure (genErrors ¬p) + _ → failure "Unexpected certificate in DELEG" + Computational-DELEG .completeness de stᵈ (delegate c mv mc d) + s' (DELEG-delegate p) rewrite dec-yes (¿ (c ∉ dom (DState.rewards stᵈ) → d ≡ DelegEnv.pparams de .PParams.keyDeposit) + × (c ∈ dom (DState.rewards stᵈ) → d ≡ 0) + × mv ∈ mapˢ (just ∘ vDelegCredential) (DelegEnv.delegatees de) ∪ fromList ( nothing ∷ just vDelegAbstain ∷ just vDelegNoConfidence ∷ [] ) + × mc ∈ mapˢ just (dom (DelegEnv.pools de)) ∪ ❴ nothing ❵ + ¿) p .proj₂ = refl + Computational-DELEG .completeness de stᵈ (dereg c d) _ (DELEG-dereg p) + rewrite dec-yes (¿ (c , 0) ∈ (DState.rewards stᵈ) ¿) p .proj₂ = refl + Computational-DELEG .completeness de stᵈ (reg c d) _ (DELEG-reg p) + rewrite dec-yes (¿ c ∉ dom (DState.rewards stᵈ) × (d ≡ DelegEnv.pparams de .PParams.keyDeposit ⊎ d ≡ 0) ¿) p .proj₂ = refl + + Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String + Computational-POOL .computeProof _ stᵖ (regpool c _) = + let open PState stᵖ in + case ¬? (c ∈? dom pools) of λ where + (yes p) → success (-, POOL-regpool p) + (no ¬p) → failure (genErrors ¬p) + Computational-POOL .computeProof _ _ (retirepool c e) = success (-, POOL-retirepool) + Computational-POOL .computeProof _ _ _ = failure "Unexpected certificate in POOL" + Computational-POOL .completeness _ stᵖ (regpool c _) _ (POOL-regpool ¬p) + rewrite dec-no (c ∈? dom (PState.pools stᵖ)) ¬p = refl + Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl + + Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_ String + Computational-GOVCERT .computeProof ce stᵍ (regdrep c d _) = + let open CertEnv ce; open PParams pp in + case ¿ (d ≡ drepDeposit × c ∉ dom (GState.dreps stᵍ)) + ⊎ (d ≡ 0 × c ∈ dom (GState.dreps stᵍ)) ¿ of λ where + (yes p) → success (-, GOVCERT-regdrep p) + (no ¬p) → failure (genErrors ¬p) + Computational-GOVCERT .computeProof _ stᵍ (deregdrep c _) = + let open GState stᵍ in + case c ∈? dom dreps of λ where + (yes p) → success (-, GOVCERT-deregdrep p) + (no ¬p) → failure (genErrors ¬p) + Computational-GOVCERT .computeProof ce stᵍ (ccreghot c _) = + let open CertEnv ce; open GState stᵍ in + case ¿ ((c , nothing) ∉ ccHotKeys ˢ) × c ∈ coldCreds ¿ of λ where + (yes p) → success (-, GOVCERT-ccreghot p) + (no ¬p) → failure (genErrors ¬p) + Computational-GOVCERT .computeProof _ _ _ = failure "Unexpected certificate in GOVCERT" + Computational-GOVCERT .completeness ce stᵍ + (regdrep c d _) _ (GOVCERT-regdrep p) + rewrite dec-yes + ¿ (let open CertEnv ce; open PParams pp; open GState stᵍ in + (d ≡ drepDeposit × c ∉ dom dreps) ⊎ (d ≡ 0 × c ∈ dom dreps)) + ¿ p .proj₂ = refl + Computational-GOVCERT .completeness _ stᵍ + (deregdrep c _) _ (GOVCERT-deregdrep p) + rewrite dec-yes (c ∈? dom (GState.dreps stᵍ)) p .proj₂ = refl + Computational-GOVCERT .completeness ce stᵍ + (ccreghot c _) _ (GOVCERT-ccreghot p) + rewrite dec-yes (¿ (((c , nothing) ∉ (GState.ccHotKeys stᵍ) ˢ) × c ∈ CertEnv.coldCreds ce) ¿) p .proj₂ = refl + + Computational-CERT : Computational _⊢_⇀⦇_,CERT⦈_ String + Computational-CERT .computeProof ce cs dCert + with computeProof ⟦ CertEnv.pp ce , PState.pools (pState cs) , dom (GState.dreps (gState cs)) ⟧ (dState cs) dCert + | computeProof (CertEnv.pp ce) (pState cs) dCert | computeProof ce (gState cs) dCert + ... | success (_ , h) | _ | _ = success (-, CERT-deleg h) + ... | failure _ | success (_ , h) | _ = success (-, CERT-pool h) + ... | failure _ | failure _ | success (_ , h) = success (-, CERT-vdel h) + ... | failure e₁ | failure e₂ | failure e₃ = failure $ + "DELEG: " <> e₁ <> "\nPOOL: " <> e₂ <> "\nVDEL: " <> e₃ + Computational-CERT .completeness ce cs + dCert@(delegate c mv mc d) cs' (CERT-deleg h) + with computeProof ⟦ CertEnv.pp ce , PState.pools (pState cs) , dom (GState.dreps (gState cs)) ⟧ (dState cs) dCert | completeness _ _ _ _ h + ... | success _ | refl = refl + Computational-CERT .completeness ce cs + dCert@(reg c d) cs' (CERT-deleg h) + with computeProof ⟦ CertEnv.pp ce , PState.pools (pState cs) , dom (GState.dreps (gState cs)) ⟧ (dState cs) dCert | completeness _ _ _ _ h + ... | success _ | refl = refl + Computational-CERT .completeness ce cs + dCert@(dereg c _) cs' (CERT-deleg h) + with computeProof ⟦ CertEnv.pp ce , PState.pools (pState cs) , dom (GState.dreps (gState cs)) ⟧ (dState cs) dCert | completeness _ _ _ _ h + ... | success _ | refl = refl + Computational-CERT .completeness ce cs + dCert@(regpool c poolParams) cs' (CERT-pool h) + with computeProof (CertEnv.pp ce) (pState cs) dCert | completeness _ _ _ _ h + ... | success _ | refl = refl + Computational-CERT .completeness ce cs + dCert@(retirepool c e) cs' (CERT-pool h) + with completeness _ _ _ _ h + ... | refl = refl + Computational-CERT .completeness ce cs + dCert@(regdrep c d an) + cs' (CERT-vdel h) + with computeProof ce (gState cs) dCert | completeness _ _ _ _ h + ... | success _ | refl = refl + Computational-CERT .completeness ce cs + dCert@(deregdrep c _) cs' (CERT-vdel h) + with computeProof ce (gState cs) dCert | completeness _ _ _ _ h + ... | success _ | refl = refl + Computational-CERT .completeness ce cs + dCert@(ccreghot c mkh) cs' (CERT-vdel h) + with computeProof ce (gState cs) dCert | completeness _ _ _ _ h + ... | success _ | refl = refl + + Computational-CERTBASE : Computational _⊢_⇀⦇_,CERTBASE⦈_ String + Computational-CERTBASE .computeProof ce cs _ = + let open CertEnv ce; open PParams pp + open GState (gState cs); open DState (dState cs) + refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList votes) + refreshedDReps = mapValueRestricted (const (CertEnv.epoch ce + drepActivity)) dreps refresh + in case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs + × mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where + (yes p) → success (-, CERT-base p) + (no ¬p) → failure (genErrors ¬p) + Computational-CERTBASE .completeness ce st _ st' (CERT-base p) + rewrite let dState = CertState.dState st; open DState dState in + dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom (CertEnv.wdrls ce))) ⊆ dom voteDelegs + × mapˢ (map₁ RwdAddr.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿ + p .proj₂ = refl + +Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String +Computational-CERTS = it diff --git a/src/Ledger/Conway/Specification/Chain/Properties.agda b/src/Ledger/Conway/Specification/Chain/Properties.agda index 1414a03b9..ede859ebc 100644 --- a/src/Ledger/Conway/Specification/Chain/Properties.agda +++ b/src/Ledger/Conway/Specification/Chain/Properties.agda @@ -1,48 +1,9 @@ {-# OPTIONS --safe #-} -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open import Ledger.Conway.Specification.Abstract using (AbstractFunctions) +module Ledger.Conway.Specification.Chain.Properties where -module Ledger.Conway.Specification.Chain.Properties - (txs : _) (open TransactionStructure txs) - (abs : AbstractFunctions txs) (open AbstractFunctions abs) - where -open import Ledger.Conway.Specification.BlockBody.Properties txs abs -open import Ledger.Conway.Specification.Chain txs abs -open import Ledger.Conway.Specification.Enact govStructure using (EnactState) -open import Ledger.Conway.Specification.Epoch txs abs -open import Ledger.Conway.Specification.Epoch.Properties txs abs -open import Ledger.Conway.Specification.Ledger txs abs -open import Ledger.Conway.Specification.RewardUpdate txs abs -open import Ledger.Conway.Specification.RewardUpdate.Properties txs abs -open import Ledger.Prelude - -open Computational ⦃...⦄ - -module _ - (nes : NewEpochState) - (open EpochState (NewEpochState.epochState nes) using (ls) renaming (es to es')) - (open EnactState es' using (pparams)) - (open PParams ∣ pparams ∣ using (maxRefScriptSizePerBlock)) - (ts : List Tx) - where - refScriptSize≤?Bound : Dec (totalRefScriptsSize ls ts ≤ maxRefScriptSizePerBlock) - refScriptSize≤?Bound = totalRefScriptsSize ls ts ≤? maxRefScriptSizePerBlock - -instance - Computational-CHAIN : Computational _⊢_⇀⦇_,CHAIN⦈_ String - Computational-CHAIN .computeProof Γ s b = do - nes , tickStep ← map₁ ⊥-elim $ computeProof {STS = _⊢_⇀⦇_,TICK⦈_} _ _ _ - (_ , _) , bbStep ← computeProof _ (LStateOf nes , nes .NewEpochState.bcur) b - case refScriptSize≤?Bound nes (b .Block.ts) of λ where - (no ¬p) → failure "totalRefScriptsSize > maxRefScriptSizePerBlock" - (yes p) → success (_ , CHAIN (p , tickStep , bbStep)) - - Computational-CHAIN .completeness _ s b _ (CHAIN {nes = nes} (p , tickStep , bbStep)) - with recomputeProof tickStep | completeness _ _ _ _ tickStep - ... | success _ | refl - with recomputeProof bbStep | completeness _ _ _ _ bbStep - ... | success _ | refl - with refScriptSize≤?Bound nes (Block.ts b) - ... | yes p = refl - ... | no ¬p = ⊥-elim (¬p p) +open import Ledger.Conway.Specification.Chain.Properties.Computational +open import Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds +open import Ledger.Conway.Specification.Chain.Properties.EpochStep +open import Ledger.Conway.Specification.Chain.Properties.GovDepsMatch +open import Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed diff --git a/src/Ledger/Conway/Specification/Chain/Properties/Computational.agda b/src/Ledger/Conway/Specification/Chain/Properties/Computational.agda new file mode 100644 index 000000000..7b89739ed --- /dev/null +++ b/src/Ledger/Conway/Specification/Chain/Properties/Computational.agda @@ -0,0 +1,47 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open import Ledger.Conway.Specification.Abstract using (AbstractFunctions) + +module Ledger.Conway.Specification.Chain.Properties.Computational + (txs : _) (open TransactionStructure txs) + (abs : AbstractFunctions txs) (open AbstractFunctions abs) + where +open import Ledger.Conway.Specification.BlockBody.Properties txs abs +open import Ledger.Conway.Specification.Chain txs abs +open import Ledger.Conway.Specification.Enact govStructure using (EnactState) +open import Ledger.Conway.Specification.Epoch txs abs +open import Ledger.Conway.Specification.Ledger txs abs +open import Ledger.Conway.Specification.RewardUpdate txs abs +open import Ledger.Conway.Specification.RewardUpdate.Properties txs abs +open import Ledger.Prelude + +open Computational ⦃...⦄ + +module _ + (nes : NewEpochState) + (open EpochState (NewEpochState.epochState nes) using (ls) renaming (es to es')) + (open EnactState es' using (pparams)) + (open PParams ∣ pparams ∣ using (maxRefScriptSizePerBlock)) + (ts : List Tx) + where + refScriptSize≤?Bound : Dec (totalRefScriptsSize ls ts ≤ maxRefScriptSizePerBlock) + refScriptSize≤?Bound = totalRefScriptsSize ls ts ≤? maxRefScriptSizePerBlock + +instance + Computational-CHAIN : Computational _⊢_⇀⦇_,CHAIN⦈_ String + Computational-CHAIN .computeProof Γ s b = do + nes , tickStep ← map₁ ⊥-elim $ computeProof {STS = _⊢_⇀⦇_,TICK⦈_} _ _ _ + (_ , _) , bbStep ← computeProof _ (LStateOf nes , nes .NewEpochState.bcur) b + case refScriptSize≤?Bound nes (b .Block.ts) of λ where + (no ¬p) → failure "totalRefScriptsSize > maxRefScriptSizePerBlock" + (yes p) → success (_ , CHAIN (p , tickStep , bbStep)) + + Computational-CHAIN .completeness _ s b _ (CHAIN {nes = nes} (p , tickStep , bbStep)) + with recomputeProof tickStep | completeness _ _ _ _ tickStep + ... | success _ | refl + with recomputeProof bbStep | completeness _ _ _ _ bbStep + ... | success _ | refl + with refScriptSize≤?Bound nes (Block.ts b) + ... | yes p = refl + ... | no ¬p = ⊥-elim (¬p p) diff --git a/src/Ledger/Conway/Specification/Chain/Properties/GovDepsMatch.lagda.md b/src/Ledger/Conway/Specification/Chain/Properties/GovDepsMatch.lagda.md index a45897285..7ed4f7a8f 100644 --- a/src/Ledger/Conway/Specification/Chain/Properties/GovDepsMatch.lagda.md +++ b/src/Ledger/Conway/Specification/Chain/Properties/GovDepsMatch.lagda.md @@ -17,8 +17,8 @@ open import Ledger.Conway.Specification.Enact govStructure open import Ledger.Conway.Specification.Epoch txs abs open import Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch txs abs open import Ledger.Conway.Specification.Ledger txs abs -open import Ledger.Conway.Specification.Ledger.Properties txs abs open import Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch txs abs +open import Ledger.Conway.Specification.Ledger.Properties.Setoid txs abs open import Ledger.Prelude hiding (map) renaming (mapˢ to map) open import Ledger.Conway.Specification.RewardUpdate txs abs diff --git a/src/Ledger/Conway/Specification/Epoch/Properties.agda b/src/Ledger/Conway/Specification/Epoch/Properties.agda index ca7ce762d..4d53ecb03 100644 --- a/src/Ledger/Conway/Specification/Epoch/Properties.agda +++ b/src/Ledger/Conway/Specification/Epoch/Properties.agda @@ -1,168 +1,8 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude -open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Abstract +module Ledger.Conway.Specification.Epoch.Properties where -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 = ⟦ u0 .utxoSt' , acnt , cs .dState , cs .pState ⟧ - 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 - ( SNAP-total .proj₂ - , RATIFIES-total' .proj₂ - , POOLREAP-total prs .proj₂) - - private - EPOCH-state : Snapshots → RatifyState → PoolReapState → EpochState - EPOCH-state ss fut' (⟦ utxoSt'' , acnt' , dState' , pState' ⟧ᵖ) = - let - EPOCHUpdates es govSt' dState'' gState' _ acnt'' = - EPOCH-updates fut ls dState' acnt' - certState' = ⟦ dState'' , pState' , gState' ⟧ᶜˢ - in - record - { acnt = acnt'' - ; ss = ss - ; ls = ⟦ utxoSt'' , govSt' , certState' ⟧ˡ - ; 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'' : ⟦ utxoSt''₁ , acnt'₁ , dState'₁ , pState'₁ ⟧ᵖ ≡ - ⟦ utxoSt''₂ , acnt'₂ , dState'₂ , pState'₂ ⟧ - 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 ] = ⟦ e , _ , _ , EPOCH-total' .proj₁ , nothing , _ ⟧ - , NEWEPOCH-New (p , EPOCH-total' .proj₂) - ... | yes p | nothing | PE.[ refl ] = ⟦ e , _ , _ , proj₁ EPOCH-total' , nothing , _ ⟧ - , 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 | h - 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) +open import Ledger.Conway.Specification.Epoch.Properties.Computational +open import Ledger.Conway.Specification.Epoch.Properties.ConstRwds +open import Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch +open import Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda b/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda new file mode 100644 index 000000000..ef93aa15b --- /dev/null +++ b/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda @@ -0,0 +1,168 @@ +{-# 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.Computational + (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 = ⟦ u0 .utxoSt' , acnt , cs .dState , cs .pState ⟧ + 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 + ( SNAP-total .proj₂ + , RATIFIES-total' .proj₂ + , POOLREAP-total prs .proj₂) + + private + EPOCH-state : Snapshots → RatifyState → PoolReapState → EpochState + EPOCH-state ss fut' (⟦ utxoSt'' , acnt' , dState' , pState' ⟧ᵖ) = + let + EPOCHUpdates es govSt' dState'' gState' _ acnt'' = + EPOCH-updates fut ls dState' acnt' + certState' = ⟦ dState'' , pState' , gState' ⟧ᶜˢ + in + record + { acnt = acnt'' + ; ss = ss + ; ls = ⟦ utxoSt'' , govSt' , certState' ⟧ˡ + ; 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'' : ⟦ utxoSt''₁ , acnt'₁ , dState'₁ , pState'₁ ⟧ᵖ ≡ + ⟦ utxoSt''₂ , acnt'₂ , dState'₂ , pState'₂ ⟧ + 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 ] = ⟦ e , _ , _ , EPOCH-total' .proj₁ , nothing , _ ⟧ + , NEWEPOCH-New (p , EPOCH-total' .proj₂) + ... | yes p | nothing | PE.[ refl ] = ⟦ e , _ , _ , proj₁ EPOCH-total' , nothing , _ ⟧ + , 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 | h + 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) diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md b/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md index e21885763..32edcc19e 100644 --- a/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md +++ b/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md @@ -15,7 +15,7 @@ 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.Ledger.Properties.Setoid 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) diff --git a/src/Ledger/Conway/Specification/Gov/Properties.agda b/src/Ledger/Conway/Specification/Gov/Properties.agda index ca824bfbe..435aa6fa6 100644 --- a/src/Ledger/Conway/Specification/Gov/Properties.agda +++ b/src/Ledger/Conway/Specification/Gov/Properties.agda @@ -1,171 +1,6 @@ {-# OPTIONS --safe #-} -open import Ledger.Conway.Specification.Gov.Base -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +module Ledger.Conway.Specification.Gov.Properties where -module Ledger.Conway.Specification.Gov.Properties - (txs : _) (open TransactionStructure txs using (govStructure)) - (open GovStructure govStructure hiding (epoch)) where - -open import Ledger.Prelude hiding (Any; any?) - -open import Axiom.Set.Properties - -open import Ledger.Conway.Specification.Enact govStructure -open import Ledger.Conway.Specification.Gov txs -open import Ledger.Conway.Specification.Gov.Actions govStructure hiding (yes; no) -open import Ledger.Conway.Specification.Ratify txs - -import Data.List.Membership.Propositional as P -open import Data.List.Membership.Propositional.Properties -open import Data.List.Relation.Unary.All using (all?; All) -open import Data.List.Relation.Unary.Any hiding (map) -open import Data.List.Relation.Unary.Unique.Propositional -open import Data.Maybe.Properties -open import Relation.Binary using (IsEquivalence) - -open import Tactic.Defaults -open import stdlib-meta.Tactic.GenError - -open Equivalence -open GovActionState -open Inverse - -lookupActionId : (pparams : PParams) (role : GovRole) (aid : GovActionID) (epoch : Epoch) (s : GovState) → - Dec (Any (λ (aid' , ast) → aid ≡ aid' × canVote pparams (action ast) role × ¬ (expired epoch ast)) s) -lookupActionId pparams role aid epoch = - let instance _ = λ {e ga} → ⁇ (expired? e ga) - in any? λ _ → ¿ _ ¿ - -private - isUpdateCommittee : (a : GovAction) → Dec (∃[ new ] ∃[ rem ] ∃[ q ] a ≡ ⟦ UpdateCommittee , (new , rem , q) ⟧ᵍᵃ) - isUpdateCommittee ⟦ NoConfidence , _ ⟧ᵍᵃ = no λ() - isUpdateCommittee ⟦ UpdateCommittee , (new , rem , q) ⟧ᵍᵃ = yes (new , rem , q , refl) - isUpdateCommittee ⟦ NewConstitution , _ ⟧ᵍᵃ = no λ() - isUpdateCommittee ⟦ TriggerHardFork , _ ⟧ᵍᵃ = no λ() - isUpdateCommittee ⟦ ChangePParams , _ ⟧ᵍᵃ = no λ() - isUpdateCommittee ⟦ TreasuryWithdrawal , _ ⟧ᵍᵃ = no λ() - isUpdateCommittee ⟦ Info , _ ⟧ᵍᵃ = no λ() - - hasPrev : ∀ x v → Dec (∃[ v' ] x .action ≡ ⟦ TriggerHardFork , v' ⟧ᵍᵃ × pvCanFollow v' v) - hasPrev record { action = ⟦ NoConfidence , _ ⟧ᵍᵃ} v = no λ () - hasPrev record { action = ⟦ UpdateCommittee , _ ⟧ᵍᵃ} v = no λ () - hasPrev record { action = ⟦ NewConstitution , _ ⟧ᵍᵃ} v = no λ () - hasPrev record { action = ⟦ TriggerHardFork , v' ⟧ᵍᵃ} v = case pvCanFollow? {v'} {v} of λ where - (yes p) → yes (-, refl , p) - (no ¬p) → no (λ where (_ , refl , h) → ¬p h) - hasPrev record { action = ⟦ ChangePParams , _ ⟧ᵍᵃ} v = no λ () - hasPrev record { action = ⟦ TreasuryWithdrawal , _ ⟧ᵍᵃ} v = no λ () - hasPrev record { action = ⟦ Info , _ ⟧ᵍᵃ} v = no λ () - -opaque - unfolding validHFAction isRegistered - - instance - validHFAction? : ∀ {p s e} → validHFAction p s e ⁇ - validHFAction? {record { action = ⟦ NoConfidence , _ ⟧ᵍᵃ}} = Dec-⊤ - validHFAction? {record { action = ⟦ UpdateCommittee , _ ⟧ᵍᵃ}} = Dec-⊤ - validHFAction? {record { action = ⟦ NewConstitution , _ ⟧ᵍᵃ}} = Dec-⊤ - validHFAction? {record { action = ⟦ TriggerHardFork , v ⟧ᵍᵃ ; prevAction = prev }} {s} {record { pv = (v' , aid') }} - with aid' ≟ prev ×-dec pvCanFollow? {v'} {v} | any? (λ (aid , x) → aid ≟ prev ×-dec hasPrev x v) s - ... | yes p | _ = ⁇ yes (inj₁ p) - ... | no _ | yes p with ((aid , x) , x∈xs , (refl , v , h)) ← P.find p = ⁇ yes (inj₂ - (x , v , to ∈-fromList x∈xs , h)) - ... | no ¬p₁ | no ¬p₂ = ⁇ no λ - { (inj₁ x) → ¬p₁ x - ; (inj₂ (s , v , (h₁ , h₂ , h₃))) → ¬p₂ $ - ∃∈-Any ((prev , s) , (from ∈-fromList h₁ , refl , (v , h₂ , h₃))) } - validHFAction? {record { action = ⟦ ChangePParams , _ ⟧ᵍᵃ}} = Dec-⊤ - validHFAction? {record { action = ⟦ TreasuryWithdrawal , _ ⟧ᵍᵃ}} = Dec-⊤ - validHFAction? {record { action = ⟦ Info , _ ⟧ᵍᵃ}} = Dec-⊤ - - isRegistered? : ∀ Γ v → Dec (isRegistered Γ v) - isRegistered? _ ⟦ CC , _ ⟧ᵍᵛ = ¿ _ ∈ _ ¿ - isRegistered? _ ⟦ DRep , _ ⟧ᵍᵛ = ¿ _ ∈ _ ¿ - isRegistered? _ ⟦ SPO , _ ⟧ᵍᵛ = ¿ _ ∈ _ ¿ - -open GovVoter - -instance - Computational-GOV : Computational _⊢_⇀⦇_,GOV⦈_ String - Computational-GOV = record {Go} where - module Go Γ s where - open GovEnv (proj₁ Γ) - k = proj₂ Γ - - module GoVote sig where - open GovVote sig - - computeProof = case lookupActionId pparams (gvRole voter) gid epoch s ,′ isRegistered? (proj₁ Γ) voter of λ where - (yes p , yes p') → case Any↔ .from p of λ where - (_ , mem , refl , cV , ¬exp) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p' , ¬exp)) - (yes _ , no ¬p) → failure (genErrors ¬p) - (no ¬p , _ ) → failure (genErrors ¬p) - - completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₁ sig ,GOV⦈ s' → map proj₁ computeProof ≡ success s' - completeness s' (GOV-Vote {ast = ast} (mem , cV , reg , ¬expired)) - with lookupActionId pparams (gvRole voter) gid epoch s | isRegistered? (proj₁ Γ) voter - ... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV , ¬expired))) - ... | yes _ | no ¬p = ⊥-elim $ ¬p reg - ... | yes p | yes q with Any↔ .from p - ... | ((_ , ast') , mem , refl , cV) = refl - - module GoProp prop where - open GovProposal prop - renaming (action to a; deposit to d; policy to p; returnAddr to addr; prevAction to prev) - open PParams pparams hiding (a) - - instance - Dec-actionWellFormed = actionWellFormed? - Dec-actionValid = actionValid? - {-# INCOHERENT Dec-actionWellFormed #-} - {-# INCOHERENT Dec-actionValid #-} - - H = ¿ actionWellFormed a - × actionValid rewardCreds p ppolicy epoch a - × d ≡ govActionDeposit - × validHFAction prop s enactState - × hasParent' enactState s (a .gaType) prev - × NetworkIdOf addr ≡ NetworkId - × CredentialOf addr ∈ rewardCreds ¿ - ,′ isUpdateCommittee a - - computeProof = case H of λ where - (yes (wf , av , dep , vHFA , HasParent' en , goodAddr , regReturn) , yes (new , rem , q , refl)) → - case ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ of λ where - (yes newOk) → success (-, GOV-Propose {_} {_} {_} {_} {_} {_} {_} {_} {_} {(new , rem , q)} (wf , av , dep , vHFA , en , goodAddr , regReturn)) - (no ¬p) → failure (genErrors ¬p) - (yes (wf , av , dep , vHFA , HasParent' en , goodAddr , returnReg) , no notNewComm) → success - (-, GOV-Propose {_} {_} {_} {_} {_} {_} {_} {_} {_} {a .gaData} (wf , av , dep , vHFA , en , goodAddr , returnReg)) - (no ¬p , _) → failure (genErrors ¬p) - - completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₂ prop ,GOV⦈ s' → map proj₁ computeProof ≡ success s' - completeness s' (GOV-Propose (wf , av , dep , vHFA , en , goodAddr)) with H - ... | (no ¬p , _) = ⊥-elim (¬p (wf , av , dep , vHFA , HasParent' en , goodAddr)) - ... | (yes (_ , _ , _ , _ , HasParent' _ , _) , no notNewComm) = refl - ... | (yes (_ , (_ , (av₁ , av₂)) , _ , _ , HasParent' _ , _) , yes (new , rem , q , refl)) - rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ (λ { x → av₁ x , av₂ }) .proj₂ = refl - - computeProof : (sig : GovVote ⊎ GovProposal) → _ - computeProof (inj₁ s) = GoVote.computeProof s - computeProof (inj₂ s) = GoProp.computeProof s - - completeness : ∀ sig s' → Γ ⊢ s ⇀⦇ sig ,GOV⦈ s' → _ - completeness (inj₁ s) = GoVote.completeness s - completeness (inj₂ s) = GoProp.completeness s - -Computational-GOVS : Computational _⊢_⇀⦇_,GOVS⦈_ String -Computational-GOVS = it - -allEnactable-singleton : ∀ {aid s es} → getHash (s .prevAction) ≡ getHashES es (GovActionTypeOf s) - → allEnactable es [ (aid , s) ] -allEnactable-singleton {aid} {s} {es} eq = helper All.∷ All.[] - where - module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence th) - - helper : enactable es (getAidPairsList [ (aid , s) ]) (aid , s) - helper with getHashES es (GovActionTypeOf s) | getHash (s .prevAction) - ... | just x | just x' with refl <- just-injective eq = - [ (aid , x) ] , proj₁ ≡ᵉ.refl , All.[] ∷ [] , inj₁ (refl , refl) - ... | just x | nothing = case eq of λ () - ... | nothing | _ = _ +open import Ledger.Conway.Specification.Gov.Properties.Computational +open import Ledger.Conway.Specification.Gov.Properties.ChangePPGroup diff --git a/src/Ledger/Conway/Specification/Gov/Properties/Computational.agda b/src/Ledger/Conway/Specification/Gov/Properties/Computational.agda new file mode 100644 index 000000000..401b11ef4 --- /dev/null +++ b/src/Ledger/Conway/Specification/Gov/Properties/Computational.agda @@ -0,0 +1,171 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Conway.Specification.Gov.Base +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + +module Ledger.Conway.Specification.Gov.Properties.Computational + (txs : _) (open TransactionStructure txs using (govStructure)) + (open GovStructure govStructure hiding (epoch)) where + +open import Ledger.Prelude hiding (Any; any?) + +open import Axiom.Set.Properties + +open import Ledger.Conway.Specification.Enact govStructure +open import Ledger.Conway.Specification.Gov txs +open import Ledger.Conway.Specification.Gov.Actions govStructure hiding (yes; no) +open import Ledger.Conway.Specification.Ratify txs + +import Data.List.Membership.Propositional as P +open import Data.List.Membership.Propositional.Properties +open import Data.List.Relation.Unary.All using (all?; All) +open import Data.List.Relation.Unary.Any hiding (map) +open import Data.List.Relation.Unary.Unique.Propositional +open import Data.Maybe.Properties +open import Relation.Binary using (IsEquivalence) + +open import Tactic.Defaults +open import stdlib-meta.Tactic.GenError + +open Equivalence +open GovActionState +open Inverse + +lookupActionId : (pparams : PParams) (role : GovRole) (aid : GovActionID) (epoch : Epoch) (s : GovState) → + Dec (Any (λ (aid' , ast) → aid ≡ aid' × canVote pparams (action ast) role × ¬ (expired epoch ast)) s) +lookupActionId pparams role aid epoch = + let instance _ = λ {e ga} → ⁇ (expired? e ga) + in any? λ _ → ¿ _ ¿ + +private + isUpdateCommittee : (a : GovAction) → Dec (∃[ new ] ∃[ rem ] ∃[ q ] a ≡ ⟦ UpdateCommittee , (new , rem , q) ⟧ᵍᵃ) + isUpdateCommittee ⟦ NoConfidence , _ ⟧ᵍᵃ = no λ() + isUpdateCommittee ⟦ UpdateCommittee , (new , rem , q) ⟧ᵍᵃ = yes (new , rem , q , refl) + isUpdateCommittee ⟦ NewConstitution , _ ⟧ᵍᵃ = no λ() + isUpdateCommittee ⟦ TriggerHardFork , _ ⟧ᵍᵃ = no λ() + isUpdateCommittee ⟦ ChangePParams , _ ⟧ᵍᵃ = no λ() + isUpdateCommittee ⟦ TreasuryWithdrawal , _ ⟧ᵍᵃ = no λ() + isUpdateCommittee ⟦ Info , _ ⟧ᵍᵃ = no λ() + + hasPrev : ∀ x v → Dec (∃[ v' ] x .action ≡ ⟦ TriggerHardFork , v' ⟧ᵍᵃ × pvCanFollow v' v) + hasPrev record { action = ⟦ NoConfidence , _ ⟧ᵍᵃ} v = no λ () + hasPrev record { action = ⟦ UpdateCommittee , _ ⟧ᵍᵃ} v = no λ () + hasPrev record { action = ⟦ NewConstitution , _ ⟧ᵍᵃ} v = no λ () + hasPrev record { action = ⟦ TriggerHardFork , v' ⟧ᵍᵃ} v = case pvCanFollow? {v'} {v} of λ where + (yes p) → yes (-, refl , p) + (no ¬p) → no (λ where (_ , refl , h) → ¬p h) + hasPrev record { action = ⟦ ChangePParams , _ ⟧ᵍᵃ} v = no λ () + hasPrev record { action = ⟦ TreasuryWithdrawal , _ ⟧ᵍᵃ} v = no λ () + hasPrev record { action = ⟦ Info , _ ⟧ᵍᵃ} v = no λ () + +opaque + unfolding validHFAction isRegistered + + instance + validHFAction? : ∀ {p s e} → validHFAction p s e ⁇ + validHFAction? {record { action = ⟦ NoConfidence , _ ⟧ᵍᵃ}} = Dec-⊤ + validHFAction? {record { action = ⟦ UpdateCommittee , _ ⟧ᵍᵃ}} = Dec-⊤ + validHFAction? {record { action = ⟦ NewConstitution , _ ⟧ᵍᵃ}} = Dec-⊤ + validHFAction? {record { action = ⟦ TriggerHardFork , v ⟧ᵍᵃ ; prevAction = prev }} {s} {record { pv = (v' , aid') }} + with aid' ≟ prev ×-dec pvCanFollow? {v'} {v} | any? (λ (aid , x) → aid ≟ prev ×-dec hasPrev x v) s + ... | yes p | _ = ⁇ yes (inj₁ p) + ... | no _ | yes p with ((aid , x) , x∈xs , (refl , v , h)) ← P.find p = ⁇ yes (inj₂ + (x , v , to ∈-fromList x∈xs , h)) + ... | no ¬p₁ | no ¬p₂ = ⁇ no λ + { (inj₁ x) → ¬p₁ x + ; (inj₂ (s , v , (h₁ , h₂ , h₃))) → ¬p₂ $ + ∃∈-Any ((prev , s) , (from ∈-fromList h₁ , refl , (v , h₂ , h₃))) } + validHFAction? {record { action = ⟦ ChangePParams , _ ⟧ᵍᵃ}} = Dec-⊤ + validHFAction? {record { action = ⟦ TreasuryWithdrawal , _ ⟧ᵍᵃ}} = Dec-⊤ + validHFAction? {record { action = ⟦ Info , _ ⟧ᵍᵃ}} = Dec-⊤ + + isRegistered? : ∀ Γ v → Dec (isRegistered Γ v) + isRegistered? _ ⟦ CC , _ ⟧ᵍᵛ = ¿ _ ∈ _ ¿ + isRegistered? _ ⟦ DRep , _ ⟧ᵍᵛ = ¿ _ ∈ _ ¿ + isRegistered? _ ⟦ SPO , _ ⟧ᵍᵛ = ¿ _ ∈ _ ¿ + +open GovVoter + +instance + Computational-GOV : Computational _⊢_⇀⦇_,GOV⦈_ String + Computational-GOV = record {Go} where + module Go Γ s where + open GovEnv (proj₁ Γ) + k = proj₂ Γ + + module GoVote sig where + open GovVote sig + + computeProof = case lookupActionId pparams (gvRole voter) gid epoch s ,′ isRegistered? (proj₁ Γ) voter of λ where + (yes p , yes p') → case Any↔ .from p of λ where + (_ , mem , refl , cV , ¬exp) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p' , ¬exp)) + (yes _ , no ¬p) → failure (genErrors ¬p) + (no ¬p , _ ) → failure (genErrors ¬p) + + completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₁ sig ,GOV⦈ s' → map proj₁ computeProof ≡ success s' + completeness s' (GOV-Vote {ast = ast} (mem , cV , reg , ¬expired)) + with lookupActionId pparams (gvRole voter) gid epoch s | isRegistered? (proj₁ Γ) voter + ... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV , ¬expired))) + ... | yes _ | no ¬p = ⊥-elim $ ¬p reg + ... | yes p | yes q with Any↔ .from p + ... | ((_ , ast') , mem , refl , cV) = refl + + module GoProp prop where + open GovProposal prop + renaming (action to a; deposit to d; policy to p; returnAddr to addr; prevAction to prev) + open PParams pparams hiding (a) + + instance + Dec-actionWellFormed = actionWellFormed? + Dec-actionValid = actionValid? + {-# INCOHERENT Dec-actionWellFormed #-} + {-# INCOHERENT Dec-actionValid #-} + + H = ¿ actionWellFormed a + × actionValid rewardCreds p ppolicy epoch a + × d ≡ govActionDeposit + × validHFAction prop s enactState + × hasParent' enactState s (a .gaType) prev + × NetworkIdOf addr ≡ NetworkId + × CredentialOf addr ∈ rewardCreds ¿ + ,′ isUpdateCommittee a + + computeProof = case H of λ where + (yes (wf , av , dep , vHFA , HasParent' en , goodAddr , regReturn) , yes (new , rem , q , refl)) → + case ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ of λ where + (yes newOk) → success (-, GOV-Propose {_} {_} {_} {_} {_} {_} {_} {_} {_} {(new , rem , q)} (wf , av , dep , vHFA , en , goodAddr , regReturn)) + (no ¬p) → failure (genErrors ¬p) + (yes (wf , av , dep , vHFA , HasParent' en , goodAddr , returnReg) , no notNewComm) → success + (-, GOV-Propose {_} {_} {_} {_} {_} {_} {_} {_} {_} {a .gaData} (wf , av , dep , vHFA , en , goodAddr , returnReg)) + (no ¬p , _) → failure (genErrors ¬p) + + completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₂ prop ,GOV⦈ s' → map proj₁ computeProof ≡ success s' + completeness s' (GOV-Propose (wf , av , dep , vHFA , en , goodAddr)) with H + ... | (no ¬p , _) = ⊥-elim (¬p (wf , av , dep , vHFA , HasParent' en , goodAddr)) + ... | (yes (_ , _ , _ , _ , HasParent' _ , _) , no notNewComm) = refl + ... | (yes (_ , (_ , (av₁ , av₂)) , _ , _ , HasParent' _ , _) , yes (new , rem , q , refl)) + rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ (λ { x → av₁ x , av₂ }) .proj₂ = refl + + computeProof : (sig : GovVote ⊎ GovProposal) → _ + computeProof (inj₁ s) = GoVote.computeProof s + computeProof (inj₂ s) = GoProp.computeProof s + + completeness : ∀ sig s' → Γ ⊢ s ⇀⦇ sig ,GOV⦈ s' → _ + completeness (inj₁ s) = GoVote.completeness s + completeness (inj₂ s) = GoProp.completeness s + +Computational-GOVS : Computational _⊢_⇀⦇_,GOVS⦈_ String +Computational-GOVS = it + +allEnactable-singleton : ∀ {aid s es} → getHash (s .prevAction) ≡ getHashES es (GovActionTypeOf s) + → allEnactable es [ (aid , s) ] +allEnactable-singleton {aid} {s} {es} eq = helper All.∷ All.[] + where + module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence th) + + helper : enactable es (getAidPairsList [ (aid , s) ]) (aid , s) + helper with getHashES es (GovActionTypeOf s) | getHash (s .prevAction) + ... | just x | just x' with refl <- just-injective eq = + [ (aid , x) ] , proj₁ ≡ᵉ.refl , All.[] ∷ [] , inj₁ (refl , refl) + ... | just x | nothing = case eq of λ () + ... | nothing | _ = _ diff --git a/src/Ledger/Conway/Specification/Ledger/Properties.agda b/src/Ledger/Conway/Specification/Ledger/Properties.agda new file mode 100644 index 000000000..011bb30c2 --- /dev/null +++ b/src/Ledger/Conway/Specification/Ledger/Properties.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --safe #-} + +module Ledger.Conway.Specification.Ledger.Properties where + +open import Ledger.Conway.Specification.Ledger.Properties.Computational +open import Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch +open import Ledger.Conway.Specification.Ledger.Properties.PoV +open import Ledger.Conway.Specification.Ledger.Properties.Setoid diff --git a/src/Ledger/Conway/Specification/Ledger/Properties/Computational.lagda b/src/Ledger/Conway/Specification/Ledger/Properties/Computational.lagda new file mode 100644 index 000000000..bc2ea88f4 --- /dev/null +++ b/src/Ledger/Conway/Specification/Ledger/Properties/Computational.lagda @@ -0,0 +1,77 @@ +\begin{code}[hide] +{-# OPTIONS --safe #-} + +open import Ledger.Conway.Specification.Transaction +open import Ledger.Conway.Specification.Abstract +import Ledger.Conway.Specification.Certs + +module Ledger.Conway.Specification.Ledger.Properties.Computational + (txs : _) (open TransactionStructure txs) (open Ledger.Conway.Specification.Certs govStructure) + (abs : AbstractFunctions txs) (open AbstractFunctions abs) + where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Certs.Properties.Computational govStructure +open import Ledger.Conway.Specification.Gov txs +open import Ledger.Conway.Specification.Gov.Properties.Computational txs +open import Ledger.Conway.Specification.Ledger txs abs +open import Ledger.Conway.Specification.Utxo txs abs +open import Ledger.Conway.Specification.Utxow txs abs +open import Ledger.Conway.Specification.Utxow.Properties txs abs + +open import Data.Bool.Properties using (¬-not) + +-- ** Proof that LEDGER is computational. + +instance + _ = Monad-ComputationResult + + Computational-LEDGER : Computational _⊢_⇀⦇_,LEDGER⦈_ String + Computational-LEDGER = record {go} + where + open Computational ⦃...⦄ renaming (computeProof to comp; completeness to complete) + computeUtxow = comp {STS = _⊢_⇀⦇_,UTXOW⦈_} + computeCerts = comp {STS = _⊢_⇀⦇_,CERTS⦈_} + computeGov = comp {STS = _⊢_⇀⦇_,GOVS⦈_} + + module go + (Γ : LEnv) (let open LEnv Γ) + (s : LState) (let open LState s) + (tx : Tx) (let open Tx tx renaming (body to txb); open TxBody txb) + where + utxoΓ = UTxOEnv ∋ record { LEnv Γ } + certΓ = CertEnv ∋ ⟦ epoch slot , pparams , txGovVotes , txWithdrawals , _ ⟧ + govΓ : CertState → GovEnv + govΓ = λ certState → ⟦ txId , epoch slot , pparams , ppolicy , enactState , certState , _ ⟧ + + computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s') + computeProof = case isValid ≟ true of λ where + (yes p) → do + (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx + (certSt' , certStep) ← computeCerts certΓ certState txCerts + (govSt' , govStep) ← computeGov (govΓ certSt') (rmOrphanDRepVotes certSt' govSt) (txgov txb) + success (_ , LEDGER-V⋯ p utxoStep certStep govStep) + (no ¬p) → do + (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx + success (_ , LEDGER-I⋯ (¬-not ¬p) utxoStep) + + completeness : ∀ s' → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → (proj₁ <$> computeProof) ≡ success s' + completeness ledgerSt (LEDGER-V⋯ v utxoStep certStep govStep) + with isValid ≟ true + ... | no ¬v = contradiction v ¬v + ... | yes refl + with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep + ... | success (utxoSt' , _) | refl + with computeCerts certΓ certState txCerts | complete _ _ _ _ certStep + ... | success (certSt' , _) | refl + with computeGov (govΓ certSt') (rmOrphanDRepVotes certSt' govSt ) (txgov txb) | complete {STS = _⊢_⇀⦇_,GOVS⦈_} (govΓ certSt') _ _ _ govStep + ... | success (govSt' , _) | refl = refl + completeness ledgerSt (LEDGER-I⋯ i utxoStep) + with isValid ≟ true + ... | yes refl = case i of λ () + ... | no ¬v + with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep + ... | success (utxoSt' , _) | refl = refl + +Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_ String +Computational-LEDGERS = it diff --git a/src/Ledger/Conway/Specification/Ledger/Properties/GovDepsMatch.lagda.md b/src/Ledger/Conway/Specification/Ledger/Properties/GovDepsMatch.lagda.md index 83c5752f2..31a72cbe9 100644 --- a/src/Ledger/Conway/Specification/Ledger/Properties/GovDepsMatch.lagda.md +++ b/src/Ledger/Conway/Specification/Ledger/Properties/GovDepsMatch.lagda.md @@ -13,7 +13,8 @@ module Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch open import Ledger.Conway.Specification.Certs govStructure using (DepositPurpose) open import Ledger.Conway.Specification.Ledger txs abs -open import Ledger.Conway.Specification.Ledger.Properties txs abs +open import Ledger.Conway.Specification.Ledger.Properties.Computational txs abs +open import Ledger.Conway.Specification.Ledger.Properties.Setoid txs abs open import Ledger.Prelude open import Ledger.Conway.Specification.Utxo txs abs diff --git a/src/Ledger/Conway/Specification/Ledger/Properties.lagda b/src/Ledger/Conway/Specification/Ledger/Properties/Setoid.lagda similarity index 88% rename from src/Ledger/Conway/Specification/Ledger/Properties.lagda rename to src/Ledger/Conway/Specification/Ledger/Properties/Setoid.lagda index 49eb56c07..e3cf6cc9b 100644 --- a/src/Ledger/Conway/Specification/Ledger/Properties.lagda +++ b/src/Ledger/Conway/Specification/Ledger/Properties/Setoid.lagda @@ -5,88 +5,26 @@ open import Ledger.Conway.Specification.Transaction open import Ledger.Conway.Specification.Abstract import Ledger.Conway.Specification.Certs -module Ledger.Conway.Specification.Ledger.Properties +module Ledger.Conway.Specification.Ledger.Properties.Setoid (txs : _) (open TransactionStructure txs) (open Ledger.Conway.Specification.Certs govStructure) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where -open import Ledger.Conway.Specification.Certs.Properties govStructure +open import Ledger.Prelude open import Ledger.Conway.Specification.Gov txs -open import Ledger.Conway.Specification.Gov.Properties txs open import Ledger.Conway.Specification.Ledger txs abs -open import Ledger.Prelude -open import Ledger.Conway.Specification.Ratify txs hiding (vote) open import Ledger.Conway.Specification.Utxo txs abs open import Ledger.Conway.Specification.Utxow txs abs -open import Ledger.Conway.Specification.Utxow.Properties txs abs + +-- open import Data.List using (map) +open import Data.List.Properties using (++-identityʳ; map-++) open import Axiom.Set.Properties th -open import Data.Bool.Properties using (¬-not) -open import Data.List.Properties using (++-identityʳ; map-++) open import Data.Nat.Properties using (+-0-monoid; +-identityʳ; +-suc) open import Relation.Binary using (IsEquivalence) - import Relation.Binary.Reasoning.Setoid as SetoidReasoning -open import Interface.ComputationalRelation - --- ** Proof that LEDGER is computational. - -instance - _ = Monad-ComputationResult - - Computational-LEDGER : Computational _⊢_⇀⦇_,LEDGER⦈_ String - Computational-LEDGER = record {go} - where - open Computational ⦃...⦄ renaming (computeProof to comp; completeness to complete) - computeUtxow = comp {STS = _⊢_⇀⦇_,UTXOW⦈_} - computeCerts = comp {STS = _⊢_⇀⦇_,CERTS⦈_} - computeGov = comp {STS = _⊢_⇀⦇_,GOVS⦈_} - - module go - (Γ : LEnv) (let open LEnv Γ) - (s : LState) (let open LState s) - (tx : Tx) (let open Tx tx renaming (body to txb); open TxBody txb) - where - utxoΓ = UTxOEnv ∋ record { LEnv Γ } - certΓ = CertEnv ∋ ⟦ epoch slot , pparams , txGovVotes , txWithdrawals , _ ⟧ - govΓ : CertState → GovEnv - govΓ = λ certState → ⟦ txId , epoch slot , pparams , ppolicy , enactState , certState , _ ⟧ - - computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s') - computeProof = case isValid ≟ true of λ where - (yes p) → do - (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx - (certSt' , certStep) ← computeCerts certΓ certState txCerts - (govSt' , govStep) ← computeGov (govΓ certSt') (rmOrphanDRepVotes certSt' govSt) (txgov txb) - success (_ , LEDGER-V⋯ p utxoStep certStep govStep) - (no ¬p) → do - (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx - success (_ , LEDGER-I⋯ (¬-not ¬p) utxoStep) - - completeness : ∀ s' → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → (proj₁ <$> computeProof) ≡ success s' - completeness ledgerSt (LEDGER-V⋯ v utxoStep certStep govStep) - with isValid ≟ true - ... | no ¬v = contradiction v ¬v - ... | yes refl - with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep - ... | success (utxoSt' , _) | refl - with computeCerts certΓ certState txCerts | complete _ _ _ _ certStep - ... | success (certSt' , _) | refl - with computeGov (govΓ certSt') (rmOrphanDRepVotes certSt' govSt ) (txgov txb) | complete {STS = _⊢_⇀⦇_,GOVS⦈_} (govΓ certSt') _ _ _ govStep - ... | success (govSt' , _) | refl = refl - completeness ledgerSt (LEDGER-I⋯ i utxoStep) - with isValid ≟ true - ... | yes refl = case i of λ () - ... | no ¬v - with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep - ... | success (utxoSt' , _) | refl = refl - -Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_ String -Computational-LEDGERS = it - - -- ** Proof that the set equality `govDepsMatch` (below) is a LEDGER invariant. -- Mapping a list of `GovActionID × GovActionState`s to a list of diff --git a/src/Ledger/Conway/Specification/RewardUpdate/Properties.lagda.md b/src/Ledger/Conway/Specification/RewardUpdate/Properties.lagda.md index aa20e3e52..7246dc7e4 100644 --- a/src/Ledger/Conway/Specification/RewardUpdate/Properties.lagda.md +++ b/src/Ledger/Conway/Specification/RewardUpdate/Properties.lagda.md @@ -10,7 +10,7 @@ module Ledger.Conway.Specification.RewardUpdate.Properties where open import Ledger.Conway.Specification.RewardUpdate txs abs open import Ledger.Conway.Specification.Epoch txs abs -open import Ledger.Conway.Specification.Epoch.Properties txs abs +open import Ledger.Conway.Specification.Epoch.Properties.Computational txs abs open import Ledger.Prelude open Computational ⦃...⦄ diff --git a/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.agda b/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.agda index 55fa3ffd7..81829d3f7 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.agda @@ -19,7 +19,7 @@ open TransactionStructure SVTransactionStructure open import Ledger.Core.Specification.Epoch open EpochStructure SVEpochStructure open Implementation -open import Ledger.Conway.Specification.Utxo.Properties SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -- true if redeemer is "Hello World" helloWorld' : Maybe String → Maybe String → Bool diff --git a/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda b/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda index f47576eee..66677330e 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda @@ -19,7 +19,7 @@ open TransactionStructure SVTransactionStructure open import Ledger.Core.Specification.Epoch open EpochStructure SVEpochStructure open Implementation -open import Ledger.Conway.Specification.Utxo.Properties SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -- succeed if the datum is 1 succeedIf1Datum' : Maybe ℕ → Maybe ℕ → Bool diff --git a/src/Ledger/Conway/Specification/Utxo/Properties.agda b/src/Ledger/Conway/Specification/Utxo/Properties.agda new file mode 100644 index 000000000..4695b7856 --- /dev/null +++ b/src/Ledger/Conway/Specification/Utxo/Properties.agda @@ -0,0 +1,9 @@ +{-# OPTIONS --safe #-} + +module Ledger.Conway.Specification.Utxo.Properties where + +open import Ledger.Conway.Specification.Utxo.Properties.Computational +open import Ledger.Conway.Specification.Utxo.Properties.DepositHelpers +open import Ledger.Conway.Specification.Utxo.Properties.GenMinSpend +open import Ledger.Conway.Specification.Utxo.Properties.MinSpend +open import Ledger.Conway.Specification.Utxo.Properties.PoV diff --git a/src/Ledger/Conway/Specification/Utxo/Properties.lagda b/src/Ledger/Conway/Specification/Utxo/Properties/Computational.lagda similarity index 99% rename from src/Ledger/Conway/Specification/Utxo/Properties.lagda rename to src/Ledger/Conway/Specification/Utxo/Properties/Computational.lagda index abb929323..ad329ad4c 100644 --- a/src/Ledger/Conway/Specification/Utxo/Properties.lagda +++ b/src/Ledger/Conway/Specification/Utxo/Properties/Computational.lagda @@ -7,7 +7,7 @@ open import Ledger.Conway.Specification.Abstract open import Ledger.Conway.Specification.Transaction -module Ledger.Conway.Specification.Utxo.Properties +module Ledger.Conway.Specification.Utxo.Properties.Computational (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where diff --git a/src/Ledger/Conway/Specification/Utxow/Properties.agda b/src/Ledger/Conway/Specification/Utxow/Properties.agda index a47de2033..b6869e6f4 100644 --- a/src/Ledger/Conway/Specification/Utxow/Properties.agda +++ b/src/Ledger/Conway/Specification/Utxow/Properties.agda @@ -14,7 +14,7 @@ module Ledger.Conway.Specification.Utxow.Properties open import Ledger.Conway.Specification.Utxow txs abs open import Ledger.Conway.Specification.Utxo txs abs -open import Ledger.Conway.Specification.Utxo.Properties txs abs +open import Ledger.Conway.Specification.Utxo.Properties.Computational txs abs instance Computational-UTXOW : Computational _⊢_⇀⦇_,UTXOW⦈_ String From 5cb3ce5943aebf86af3415797bafeaad80e30c96 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Thu, 25 Sep 2025 16:59:41 -0600 Subject: [PATCH 3/6] add new modules to nav And make sure Ledger/Properties/Computational.lagda doesn't result in a blank page (without "Show more Agda"). --- build-tools/static/md/nav.yml | 7 +++++++ .../Ledger/Properties/Computational.lagda | 10 ++++++++-- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/build-tools/static/md/nav.yml b/build-tools/static/md/nav.yml index d4c219412..4917a79c7 100644 --- a/build-tools/static/md/nav.yml +++ b/build-tools/static/md/nav.yml @@ -36,6 +36,7 @@ - Certs/: - Properties: Ledger.Conway.Specification.Certs.Properties.md - Properties/: + - Computational: Ledger.Conway.Specification.Certs.Properties.Computational.md - PoV: Ledger.Conway.Specification.Certs.Properties.PoV.md - PoVLemmas: Ledger.Conway.Specification.Certs.Properties.PoVLemmas.md - VoteDelegsVDeleg: Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.md @@ -43,6 +44,7 @@ - Chain/: - Properties: Ledger.Conway.Specification.Chain.Properties.md - Properties/: + - Computational: Ledger.Conway.Specification.Chain.Properties.Computational.md - CredDepsEqualDomRwds: Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds.md - EpochStep: Ledger.Conway.Specification.Chain.Properties.EpochStep.md - GovDepsMatch: Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md @@ -54,6 +56,7 @@ - Epoch/: - Properties: Ledger.Conway.Specification.Epoch.Properties.md - Properties/: + - Computational: Ledger.Conway.Specification.Epoch.Properties.Computational.md - ConstRwds: Ledger.Conway.Specification.Epoch.Properties.ConstRwds.md - GovDepsMatch: Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch.md - NoPropSameDReps: Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps.md @@ -64,13 +67,16 @@ - Actions: Ledger.Conway.Specification.Gov.Actions.md - Properties: Ledger.Conway.Specification.Gov.Properties.md - Properties/: + - Computational: Ledger.Conway.Specification.Gov.Properties.Computational.md - ChangePPGroup: Ledger.Conway.Specification.Gov.Properties.ChangePPGroup.md - Ledger.Ledger: Ledger.Conway.Specification.Ledger.md - Ledger.Ledger/: - Properties: Ledger.Conway.Specification.Ledger.Properties.md - Properties/: + - Computational: Ledger.Conway.Specification.Ledger.Properties.Computational.md - GovDepsMatch: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md - PoV: Ledger.Conway.Specification.Ledger.Properties.PoV.md + - Setoid: Ledger.Conway.Specification.Ledger.Properties.Setoid.md - PoolReap: Ledger.Conway.Specification.PoolReap.md - PParams: Ledger.Conway.Specification.PParams.md - Properties: Ledger.Conway.Specification.Properties.md @@ -96,6 +102,7 @@ - Utxo/: - Properties: Ledger.Conway.Specification.Utxo.Properties.md - Properties/: + - Computational: Ledger.Conway.Specification.Utxo.Properties.Computational.md - DepositHelpers: Ledger.Conway.Specification.Utxo.Properties.DepositHelpers.md - GenMinspend: Ledger.Conway.Specification.Utxo.Properties.GenMinSpend.md - MinSpend: Ledger.Conway.Specification.Utxo.Properties.MinSpend.md diff --git a/src/Ledger/Conway/Specification/Ledger/Properties/Computational.lagda b/src/Ledger/Conway/Specification/Ledger/Properties/Computational.lagda index bc2ea88f4..c2b529ec6 100644 --- a/src/Ledger/Conway/Specification/Ledger/Properties/Computational.lagda +++ b/src/Ledger/Conway/Specification/Ledger/Properties/Computational.lagda @@ -1,3 +1,8 @@ +\section{Ledger: Computational} +\label{sec:ledger-computational} + +This module proves that the \LEDGER{} transition system is computational. + \begin{code}[hide] {-# OPTIONS --safe #-} @@ -20,9 +25,9 @@ open import Ledger.Conway.Specification.Utxow txs abs open import Ledger.Conway.Specification.Utxow.Properties txs abs open import Data.Bool.Properties using (¬-not) +\end{code} --- ** Proof that LEDGER is computational. - +\begin{code} instance _ = Monad-ComputationResult @@ -75,3 +80,4 @@ instance Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_ String Computational-LEDGERS = it +\end{code} From d20292c859dc05082c3de88f26ac7e7dd29050cd Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 29 Sep 2025 14:38:39 -0600 Subject: [PATCH 4/6] move computational properties of Utxow --- .../Utxow/{Properties.agda => Properties/Computational.agda} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename src/Ledger/Conway/Specification/Utxow/{Properties.agda => Properties/Computational.agda} (97%) diff --git a/src/Ledger/Conway/Specification/Utxow/Properties.agda b/src/Ledger/Conway/Specification/Utxow/Properties/Computational.agda similarity index 97% rename from src/Ledger/Conway/Specification/Utxow/Properties.agda rename to src/Ledger/Conway/Specification/Utxow/Properties/Computational.agda index b6869e6f4..9f4864a88 100644 --- a/src/Ledger/Conway/Specification/Utxow/Properties.agda +++ b/src/Ledger/Conway/Specification/Utxow/Properties/Computational.agda @@ -7,7 +7,7 @@ open import Ledger.Core.Specification.Crypto open import Ledger.Conway.Specification.Abstract open import Ledger.Conway.Specification.Transaction -module Ledger.Conway.Specification.Utxow.Properties +module Ledger.Conway.Specification.Utxow.Properties.Computational (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where From 565e338af366239350ea49481c381e723fe29537 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 29 Sep 2025 15:25:49 -0600 Subject: [PATCH 5/6] incorporate Carlos's change requests --- build-tools/static/md/nav.yml | 18 +++- .../Conway/Conformance/Epoch/Properties.agda | 2 +- src/Ledger/Conway/Foreign/HSLedger/Enact.agda | 2 +- .../Conway/Foreign/HSLedger/Ratify.agda | 2 +- .../Specification/BlockBody/Properties.agda | 5 ++ .../Computational.agda} | 4 +- .../Chain/Properties/Computational.agda | 4 +- .../Chain/Properties/GovDepsMatch.lagda.md | 2 +- .../Specification/Enact/Properties.agda | 50 +---------- .../Enact/Properties/Computational.agda | 51 +++++++++++ .../Epoch/Properties/Computational.agda | 2 +- .../Epoch/Properties/GovDepsMatch.lagda.md | 2 +- .../Specification/Ledger/Properties.agda | 2 +- .../Properties/{Setoid.lagda => Base.agda} | 11 +-- .../Ledger/Properties/Computational.lagda | 2 +- .../Ledger/Properties/GovDepsMatch.lagda.md | 2 +- .../Specification/Ratify/Properties.agda | 86 +----------------- .../Ratify/Properties/Computational.agda | 88 +++++++++++++++++++ .../RewardUpdate/Properties.agda | 5 ++ .../Computational.agda} | 4 +- .../Conway/Specification/Utxo/Properties.agda | 2 +- .../{DepositHelpers.agda => Base.agda} | 5 +- ...Computational.lagda => Computational.agda} | 24 +---- .../Utxo/Properties/PoV.lagda.md | 2 +- .../Specification/Utxow/Properties.agda | 5 ++ 25 files changed, 194 insertions(+), 188 deletions(-) create mode 100644 src/Ledger/Conway/Specification/BlockBody/Properties.agda rename src/Ledger/Conway/Specification/BlockBody/{Properties.lagda.md => Properties/Computational.agda} (93%) create mode 100644 src/Ledger/Conway/Specification/Enact/Properties/Computational.agda rename src/Ledger/Conway/Specification/Ledger/Properties/{Setoid.lagda => Base.agda} (99%) create mode 100644 src/Ledger/Conway/Specification/Ratify/Properties/Computational.agda create mode 100644 src/Ledger/Conway/Specification/RewardUpdate/Properties.agda rename src/Ledger/Conway/Specification/RewardUpdate/{Properties.lagda.md => Properties/Computational.agda} (96%) rename src/Ledger/Conway/Specification/Utxo/Properties/{DepositHelpers.agda => Base.agda} (98%) rename src/Ledger/Conway/Specification/Utxo/Properties/{Computational.lagda => Computational.agda} (93%) create mode 100644 src/Ledger/Conway/Specification/Utxow/Properties.agda diff --git a/build-tools/static/md/nav.yml b/build-tools/static/md/nav.yml index 4917a79c7..a3ced7ac5 100644 --- a/build-tools/static/md/nav.yml +++ b/build-tools/static/md/nav.yml @@ -32,6 +32,8 @@ - BlockBody: Ledger.Conway.Specification.BlockBody.md - BlockBody/: - Properties: Ledger.Conway.Specification.BlockBody.Properties.md + - Properties/: + - Computational: Ledger.Conway.Specification.BlockBody.Properties.Computational.md - Certs: Ledger.Conway.Specification.Certs.md - Certs/: - Properties: Ledger.Conway.Specification.Certs.Properties.md @@ -51,7 +53,9 @@ - PParamsWellFormed: Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed.md - Enact: Ledger.Conway.Specification.Enact.md - Enact/: - - Properties: Ledger.Conway.Specification.Enact.Properties.md + - Properties: Ledger.Conway.Specification.Enact.Properties.md + - Properties/: + - Computational: Ledger.Conway.Specification.Enact.Properties.Computational.md - Epoch: Ledger.Conway.Specification.Epoch.md - Epoch/: - Properties: Ledger.Conway.Specification.Epoch.Properties.md @@ -73,20 +77,24 @@ - Ledger.Ledger/: - Properties: Ledger.Conway.Specification.Ledger.Properties.md - Properties/: + - Base: Ledger.Conway.Specification.Ledger.Properties.Base.md - Computational: Ledger.Conway.Specification.Ledger.Properties.Computational.md - GovDepsMatch: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md - PoV: Ledger.Conway.Specification.Ledger.Properties.PoV.md - - Setoid: Ledger.Conway.Specification.Ledger.Properties.Setoid.md - PoolReap: Ledger.Conway.Specification.PoolReap.md - PParams: Ledger.Conway.Specification.PParams.md - Properties: Ledger.Conway.Specification.Properties.md - Ratify: Ledger.Conway.Specification.Ratify.md - Ratify/: - Properties: Ledger.Conway.Specification.Ratify.Properties.md + - Properties/: + - Computational: Ledger.Conway.Specification.Ratify.Properties.Computational.md - Rewards: Ledger.Conway.Specification.Rewards.md - RewardUpdate: Ledger.Conway.Specification.RewardUpdate.md - RewardUpdate/: - Properties: Ledger.Conway.Specification.RewardUpdate.Properties.md + - Properties/: + - Computational: Ledger.Conway.Specification.RewardUpdate.Properties.Computational.md - Script: Ledger.Conway.Specification.Script.md - Script/: - Base: Ledger.Conway.Specification.Script.Base.md @@ -102,14 +110,16 @@ - Utxo/: - Properties: Ledger.Conway.Specification.Utxo.Properties.md - Properties/: + - Base: Ledger.Conway.Specification.Utxo.Properties.Base.md - Computational: Ledger.Conway.Specification.Utxo.Properties.Computational.md - - DepositHelpers: Ledger.Conway.Specification.Utxo.Properties.DepositHelpers.md - GenMinspend: Ledger.Conway.Specification.Utxo.Properties.GenMinSpend.md - MinSpend: Ledger.Conway.Specification.Utxo.Properties.MinSpend.md - PoV: Ledger.Conway.Specification.Utxo.Properties.PoV.md - Utxow: Ledger.Conway.Specification.Utxow.md - Utxow/: - - Properties: Ledger.Conway.Specification.Utxow.Properties.md + - Properties: Ledger.Conway.Specification.Utxow.Properties.md + - Properties/: + - Computational: Ledger.Conway.Specification.Utxow.Properties.Computational.md - Test: - Examples: Ledger.Conway.Specification.Test.Examples.md - Examples/: diff --git a/src/Ledger/Conway/Conformance/Epoch/Properties.agda b/src/Ledger/Conway/Conformance/Epoch/Properties.agda index ea1e6e9fb..1939b54d5 100644 --- a/src/Ledger/Conway/Conformance/Epoch/Properties.agda +++ b/src/Ledger/Conway/Conformance/Epoch/Properties.agda @@ -14,7 +14,7 @@ module Ledger.Conway.Conformance.Epoch.Properties open import Ledger.Conway.Conformance.Epoch txs abs open import Ledger.Conway.Conformance.Ledger txs abs open import Ledger.Conway.Specification.Ratify txs -open import Ledger.Conway.Specification.Ratify.Properties txs +open import Ledger.Conway.Specification.Ratify.Properties.Computational txs open import Ledger.Conway.Conformance.Certs govStructure open import Ledger.Conway.Conformance.Rewards txs abs diff --git a/src/Ledger/Conway/Foreign/HSLedger/Enact.agda b/src/Ledger/Conway/Foreign/HSLedger/Enact.agda index 7029acd95..e6b41aead 100644 --- a/src/Ledger/Conway/Foreign/HSLedger/Enact.agda +++ b/src/Ledger/Conway/Foreign/HSLedger/Enact.agda @@ -7,7 +7,7 @@ open import Ledger.Conway.Foreign.HSLedger.PParams open import Ledger.Conway.Foreign.HSLedger.Gov.Actions open import Ledger.Conway.Specification.Enact govStructure -open import Ledger.Conway.Specification.Enact.Properties govStructure +open import Ledger.Conway.Specification.Enact.Properties.Computational govStructure instance HsTy-EnactState = autoHsType EnactState ⊣ withConstructor "MkEnactState" diff --git a/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda b/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda index b9f90774f..b9ba857b9 100644 --- a/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda +++ b/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda @@ -14,7 +14,7 @@ import Data.Rational.Show as Rational import Foreign.Haskell.Pair as F open import Ledger.Conway.Specification.Ratify it -open import Ledger.Conway.Specification.Ratify.Properties it +open import Ledger.Conway.Specification.Ratify.Properties.Computational it instance HsTy-StakeDistrs = autoHsType StakeDistrs diff --git a/src/Ledger/Conway/Specification/BlockBody/Properties.agda b/src/Ledger/Conway/Specification/BlockBody/Properties.agda new file mode 100644 index 000000000..ed8180f2e --- /dev/null +++ b/src/Ledger/Conway/Specification/BlockBody/Properties.agda @@ -0,0 +1,5 @@ +{-# OPTIONS --safe #-} + +module Ledger.Conway.Specification.BlockBody.Properties where + +open import Ledger.Conway.Specification.BlockBody.Properties.Computational diff --git a/src/Ledger/Conway/Specification/BlockBody/Properties.lagda.md b/src/Ledger/Conway/Specification/BlockBody/Properties/Computational.agda similarity index 93% rename from src/Ledger/Conway/Specification/BlockBody/Properties.lagda.md rename to src/Ledger/Conway/Specification/BlockBody/Properties/Computational.agda index 0342ef786..19118bd91 100644 --- a/src/Ledger/Conway/Specification/BlockBody/Properties.lagda.md +++ b/src/Ledger/Conway/Specification/BlockBody/Properties/Computational.agda @@ -1,10 +1,9 @@ -```agda {-# OPTIONS --safe #-} open import Ledger.Conway.Specification.Transaction using (TransactionStructure) open import Ledger.Conway.Specification.Abstract using (AbstractFunctions) -module Ledger.Conway.Specification.BlockBody.Properties +module Ledger.Conway.Specification.BlockBody.Properties.Computational (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where @@ -26,4 +25,3 @@ instance (BBODY-Block-Body (_ , _ , lsStep)) with recomputeProof lsStep | completeness _ _ _ _ lsStep ... | success _ | refl = refl -``` diff --git a/src/Ledger/Conway/Specification/Chain/Properties/Computational.agda b/src/Ledger/Conway/Specification/Chain/Properties/Computational.agda index 7b89739ed..e7b766840 100644 --- a/src/Ledger/Conway/Specification/Chain/Properties/Computational.agda +++ b/src/Ledger/Conway/Specification/Chain/Properties/Computational.agda @@ -7,13 +7,13 @@ module Ledger.Conway.Specification.Chain.Properties.Computational (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where -open import Ledger.Conway.Specification.BlockBody.Properties txs abs +open import Ledger.Conway.Specification.BlockBody.Properties.Computational txs abs open import Ledger.Conway.Specification.Chain txs abs open import Ledger.Conway.Specification.Enact govStructure using (EnactState) open import Ledger.Conway.Specification.Epoch txs abs open import Ledger.Conway.Specification.Ledger txs abs open import Ledger.Conway.Specification.RewardUpdate txs abs -open import Ledger.Conway.Specification.RewardUpdate.Properties txs abs +open import Ledger.Conway.Specification.RewardUpdate.Properties.Computational txs abs open import Ledger.Prelude open Computational ⦃...⦄ diff --git a/src/Ledger/Conway/Specification/Chain/Properties/GovDepsMatch.lagda.md b/src/Ledger/Conway/Specification/Chain/Properties/GovDepsMatch.lagda.md index 7ed4f7a8f..003142532 100644 --- a/src/Ledger/Conway/Specification/Chain/Properties/GovDepsMatch.lagda.md +++ b/src/Ledger/Conway/Specification/Chain/Properties/GovDepsMatch.lagda.md @@ -17,8 +17,8 @@ open import Ledger.Conway.Specification.Enact govStructure open import Ledger.Conway.Specification.Epoch txs abs open import Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch txs abs open import Ledger.Conway.Specification.Ledger txs abs +open import Ledger.Conway.Specification.Ledger.Properties.Base txs abs open import Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch txs abs -open import Ledger.Conway.Specification.Ledger.Properties.Setoid txs abs open import Ledger.Prelude hiding (map) renaming (mapˢ to map) open import Ledger.Conway.Specification.RewardUpdate txs abs diff --git a/src/Ledger/Conway/Specification/Enact/Properties.agda b/src/Ledger/Conway/Specification/Enact/Properties.agda index f77a26b73..775835727 100644 --- a/src/Ledger/Conway/Specification/Enact/Properties.agda +++ b/src/Ledger/Conway/Specification/Enact/Properties.agda @@ -1,51 +1,5 @@ {-# OPTIONS --safe #-} -open import Ledger.Conway.Specification.Gov.Base +module Ledger.Conway.Specification.Enact.Properties where -module Ledger.Conway.Specification.Enact.Properties (gs : _) (open GovStructure gs) where - -open import Ledger.Prelude - -open import Ledger.Conway.Specification.Gov.Actions gs hiding (yes; no) -open import Ledger.Conway.Specification.Enact gs - -open EnactState - -open Computational ⦃...⦄ - -instance - Computational-ENACT : Computational _⊢_⇀⦇_,ENACT⦈_ String - Computational-ENACT .computeProof Γᵉ s = - let open EnactEnv Γᵉ renaming (treasury to t; epoch to e) in - λ where - ⟦ NoConfidence , _ ⟧ᵍᵃ → success (_ , Enact-NoConf) - ⟦ UpdateCommittee , (new , rem , q) ⟧ᵍᵃ → - case ¿ ∀[ term ∈ range new ] - term ≤ CCMaxTermLengthOf s +ᵉ' e ¿ of λ where - (yes p) → success (-, Enact-UpdComm - (subst (λ x → ∀[ term ∈ range new ] term ≤ x) (sym +ᵉ≡+ᵉ') p)) - (no ¬p) → failure "ENACT failed at ∀[ term ∈ range new ] term ≤ (CCMaxTermLengthOf s +ᵉ e)" - ⟦ NewConstitution , _ ⟧ᵍᵃ → success (-, Enact-NewConst) - ⟦ TriggerHardFork , _ ⟧ᵍᵃ → success (-, Enact-HF) - ⟦ ChangePParams , _ ⟧ᵍᵃ → success (-, Enact-PParams) - ⟦ Info , _ ⟧ᵍᵃ → success (-, Enact-Info) - ⟦ TreasuryWithdrawal , wdrl ⟧ᵍᵃ → - case ¿ ∑[ x ← s .withdrawals ∪⁺ wdrl ] x ≤ t ¿ of λ where - (yes p) → success (-, Enact-Wdrl p) - (no _) → failure "ENACT failed at ∑[ x ← (s .withdrawals ∪⁺ wdrl) ᶠᵐ ] x ≤ t" - Computational-ENACT .completeness Γᵉ s action _ p - with action | p - ... | ⟦ .NoConfidence , _ ⟧ᵍᵃ | Enact-NoConf = refl - ... | ⟦ .UpdateCommittee , (new , rem , q) ⟧ᵍᵃ | Enact-UpdComm p - rewrite dec-yes - (¿ ∀[ term ∈ range new ] term - ≤ CCMaxTermLengthOf s +ᵉ' EnactEnv.epoch Γᵉ ¿) - (subst (λ x → ∀[ term ∈ range new ] term ≤ x) +ᵉ≡+ᵉ' p) .proj₂ - = refl - ... | ⟦ .NewConstitution , _ ⟧ᵍᵃ | Enact-NewConst = refl - ... | ⟦ .TriggerHardFork , _ ⟧ᵍᵃ | Enact-HF = refl - ... | ⟦ .ChangePParams , _ ⟧ᵍᵃ | Enact-PParams = refl - ... | ⟦ .Info , _ ⟧ᵍᵃ | Enact-Info = refl - ... | ⟦ .TreasuryWithdrawal , wdrl ⟧ᵍᵃ | Enact-Wdrl p - rewrite dec-yes (¿ ∑[ x ← s .withdrawals ∪⁺ wdrl ] x ≤ EnactEnv.treasury Γᵉ ¿) p .proj₂ - = refl +open import Ledger.Conway.Specification.Enact.Properties.Computational diff --git a/src/Ledger/Conway/Specification/Enact/Properties/Computational.agda b/src/Ledger/Conway/Specification/Enact/Properties/Computational.agda new file mode 100644 index 000000000..be14f0eab --- /dev/null +++ b/src/Ledger/Conway/Specification/Enact/Properties/Computational.agda @@ -0,0 +1,51 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Conway.Specification.Gov.Base + +module Ledger.Conway.Specification.Enact.Properties.Computational (gs : _) (open GovStructure gs) where + +open import Ledger.Prelude + +open import Ledger.Conway.Specification.Gov.Actions gs hiding (yes; no) +open import Ledger.Conway.Specification.Enact gs + +open EnactState + +open Computational ⦃...⦄ + +instance + Computational-ENACT : Computational _⊢_⇀⦇_,ENACT⦈_ String + Computational-ENACT .computeProof Γᵉ s = + let open EnactEnv Γᵉ renaming (treasury to t; epoch to e) in + λ where + ⟦ NoConfidence , _ ⟧ᵍᵃ → success (_ , Enact-NoConf) + ⟦ UpdateCommittee , (new , rem , q) ⟧ᵍᵃ → + case ¿ ∀[ term ∈ range new ] + term ≤ CCMaxTermLengthOf s +ᵉ' e ¿ of λ where + (yes p) → success (-, Enact-UpdComm + (subst (λ x → ∀[ term ∈ range new ] term ≤ x) (sym +ᵉ≡+ᵉ') p)) + (no ¬p) → failure "ENACT failed at ∀[ term ∈ range new ] term ≤ (CCMaxTermLengthOf s +ᵉ e)" + ⟦ NewConstitution , _ ⟧ᵍᵃ → success (-, Enact-NewConst) + ⟦ TriggerHardFork , _ ⟧ᵍᵃ → success (-, Enact-HF) + ⟦ ChangePParams , _ ⟧ᵍᵃ → success (-, Enact-PParams) + ⟦ Info , _ ⟧ᵍᵃ → success (-, Enact-Info) + ⟦ TreasuryWithdrawal , wdrl ⟧ᵍᵃ → + case ¿ ∑[ x ← s .withdrawals ∪⁺ wdrl ] x ≤ t ¿ of λ where + (yes p) → success (-, Enact-Wdrl p) + (no _) → failure "ENACT failed at ∑[ x ← (s .withdrawals ∪⁺ wdrl) ᶠᵐ ] x ≤ t" + Computational-ENACT .completeness Γᵉ s action _ p + with action | p + ... | ⟦ .NoConfidence , _ ⟧ᵍᵃ | Enact-NoConf = refl + ... | ⟦ .UpdateCommittee , (new , rem , q) ⟧ᵍᵃ | Enact-UpdComm p + rewrite dec-yes + (¿ ∀[ term ∈ range new ] term + ≤ CCMaxTermLengthOf s +ᵉ' EnactEnv.epoch Γᵉ ¿) + (subst (λ x → ∀[ term ∈ range new ] term ≤ x) +ᵉ≡+ᵉ' p) .proj₂ + = refl + ... | ⟦ .NewConstitution , _ ⟧ᵍᵃ | Enact-NewConst = refl + ... | ⟦ .TriggerHardFork , _ ⟧ᵍᵃ | Enact-HF = refl + ... | ⟦ .ChangePParams , _ ⟧ᵍᵃ | Enact-PParams = refl + ... | ⟦ .Info , _ ⟧ᵍᵃ | Enact-Info = refl + ... | ⟦ .TreasuryWithdrawal , wdrl ⟧ᵍᵃ | Enact-Wdrl p + rewrite dec-yes (¿ ∑[ x ← s .withdrawals ∪⁺ wdrl ] x ≤ EnactEnv.treasury Γᵉ ¿) p .proj₂ + = refl diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda b/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda index ef93aa15b..000d7d26a 100644 --- a/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda +++ b/src/Ledger/Conway/Specification/Epoch/Properties/Computational.agda @@ -16,7 +16,7 @@ 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.Ratify.Properties.Computational txs open import Ledger.Conway.Specification.Rewards txs abs open import Data.List using (filter) diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md b/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md index 32edcc19e..fd0efa206 100644 --- a/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md +++ b/src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md @@ -15,7 +15,7 @@ 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.Setoid txs abs +open import Ledger.Conway.Specification.Ledger.Properties.Base 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) diff --git a/src/Ledger/Conway/Specification/Ledger/Properties.agda b/src/Ledger/Conway/Specification/Ledger/Properties.agda index 011bb30c2..8061a226a 100644 --- a/src/Ledger/Conway/Specification/Ledger/Properties.agda +++ b/src/Ledger/Conway/Specification/Ledger/Properties.agda @@ -2,7 +2,7 @@ module Ledger.Conway.Specification.Ledger.Properties where +open import Ledger.Conway.Specification.Ledger.Properties.Base open import Ledger.Conway.Specification.Ledger.Properties.Computational open import Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch open import Ledger.Conway.Specification.Ledger.Properties.PoV -open import Ledger.Conway.Specification.Ledger.Properties.Setoid diff --git a/src/Ledger/Conway/Specification/Ledger/Properties/Setoid.lagda b/src/Ledger/Conway/Specification/Ledger/Properties/Base.agda similarity index 99% rename from src/Ledger/Conway/Specification/Ledger/Properties/Setoid.lagda rename to src/Ledger/Conway/Specification/Ledger/Properties/Base.agda index e3cf6cc9b..5d9c89f94 100644 --- a/src/Ledger/Conway/Specification/Ledger/Properties/Setoid.lagda +++ b/src/Ledger/Conway/Specification/Ledger/Properties/Base.agda @@ -1,11 +1,10 @@ -\begin{code}[hide] {-# OPTIONS --safe #-} open import Ledger.Conway.Specification.Transaction open import Ledger.Conway.Specification.Abstract import Ledger.Conway.Specification.Certs -module Ledger.Conway.Specification.Ledger.Properties.Setoid +module Ledger.Conway.Specification.Ledger.Properties.Base (txs : _) (open TransactionStructure txs) (open Ledger.Conway.Specification.Certs govStructure) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where @@ -39,13 +38,11 @@ isGADeposit dp = isGADepositᵇ dp ≡ true isGADepositᵇ : DepositPurpose → Bool isGADepositᵇ (GovActionDeposit _) = true isGADepositᵇ _ = false -\end{code} -\begin{code} + govDepsMatch : LState → Type govDepsMatch ls = filterˢ isGADeposit (dom (DepositsOf ls)) ≡ᵉ fromList (dpMap (GovStateOf ls)) -\end{code} -\begin{code}[hide] + module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {DepositPurpose}) pattern UTXOW-UTXOS x = UTXOW⇒UTXO (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ x) open Equivalence @@ -369,5 +366,3 @@ module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where fromList (dpMap (updateGovStates (map inj₂ txGovProposals) k govSt)) ≈˘⟨ props-dpMap-votes-invar txGovVotes txGovProposals {k} {govSt} ⟩ fromList (dpMap (updateGovStates (txgov txb) k govSt)) ∎ - -\end{code} diff --git a/src/Ledger/Conway/Specification/Ledger/Properties/Computational.lagda b/src/Ledger/Conway/Specification/Ledger/Properties/Computational.lagda index c2b529ec6..deea3fcff 100644 --- a/src/Ledger/Conway/Specification/Ledger/Properties/Computational.lagda +++ b/src/Ledger/Conway/Specification/Ledger/Properties/Computational.lagda @@ -22,7 +22,7 @@ open import Ledger.Conway.Specification.Gov.Properties.Computational txs open import Ledger.Conway.Specification.Ledger txs abs open import Ledger.Conway.Specification.Utxo txs abs open import Ledger.Conway.Specification.Utxow txs abs -open import Ledger.Conway.Specification.Utxow.Properties txs abs +open import Ledger.Conway.Specification.Utxow.Properties.Computational txs abs open import Data.Bool.Properties using (¬-not) \end{code} diff --git a/src/Ledger/Conway/Specification/Ledger/Properties/GovDepsMatch.lagda.md b/src/Ledger/Conway/Specification/Ledger/Properties/GovDepsMatch.lagda.md index 31a72cbe9..65c0068f2 100644 --- a/src/Ledger/Conway/Specification/Ledger/Properties/GovDepsMatch.lagda.md +++ b/src/Ledger/Conway/Specification/Ledger/Properties/GovDepsMatch.lagda.md @@ -13,8 +13,8 @@ module Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch open import Ledger.Conway.Specification.Certs govStructure using (DepositPurpose) open import Ledger.Conway.Specification.Ledger txs abs +open import Ledger.Conway.Specification.Ledger.Properties.Base txs abs open import Ledger.Conway.Specification.Ledger.Properties.Computational txs abs -open import Ledger.Conway.Specification.Ledger.Properties.Setoid txs abs open import Ledger.Prelude open import Ledger.Conway.Specification.Utxo txs abs diff --git a/src/Ledger/Conway/Specification/Ratify/Properties.agda b/src/Ledger/Conway/Specification/Ratify/Properties.agda index aa5a67e52..ea81f6ed2 100644 --- a/src/Ledger/Conway/Specification/Ratify/Properties.agda +++ b/src/Ledger/Conway/Specification/Ratify/Properties.agda @@ -1,87 +1,5 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude -open import Ledger.Conway.Specification.Transaction +module Ledger.Conway.Specification.Ratify.Properties where -module Ledger.Conway.Specification.Ratify.Properties (txs : _) (open TransactionStructure txs) where - -open import Ledger.Conway.Specification.Gov txs -open import Ledger.Conway.Specification.Enact govStructure -open import Ledger.Conway.Specification.Enact.Properties govStructure -open import Ledger.Conway.Specification.Ratify txs - -open Computational ⦃...⦄ hiding (computeProof; completeness) - -private - module Implementation - Γ (s : RatifyState) (sig : GovActionID × _) - (let gid , st = sig) - where - open RatifyState s - open RatifyEnv Γ; open GovActionState st - es' = compute ⟦ gid , treasury , currentEpoch ⟧ es action - acc? = accepted? Γ es st - exp? = expired? currentEpoch st - del? = delayed? (action .gaType) prevAction es delay - - opaque - acceptConds? : ∀ a → Dec (acceptConds Γ s a) - acceptConds? _ = Dec-× ⦃ ⁇ accepted? _ _ _ ⦄ - ⦃ Dec-× ⦃ Dec-→ ⦃ ⁇ delayed? _ _ _ _ ⦄ ⦄ ⦃ ⁇ Computational⇒Dec' ⦄ ⦄ .dec - - RATIFY-total : ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' - RATIFY-total - with acceptConds? sig | exp? - ... | yes p@(_ , _ , (_ , q)) | _ = -, RATIFY-Accept (p , q) - ... | no ¬p | no ¬a = -, RATIFY-Continue (¬p , ¬a) - ... | no ¬p | yes a = -, RATIFY-Reject (¬p , a) - - computeProof = success {Err = ⊥} RATIFY-total - - RATIFY-completeness : ∀ s' → Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' → RATIFY-total .proj₁ ≡ s' - RATIFY-completeness stʳ (RATIFY-Accept (p , a)) with acceptConds? sig - ... | no ¬h = ⊥-elim (¬h p) - ... | yes (_ , _ , _ , h) = cong (λ stᵉ → ⟦ stᵉ , _ , _ ⟧) $ computational⇒rightUnique Computational-ENACT h a - RATIFY-completeness s' (RATIFY-Reject (¬p , a)) - rewrite dec-no (acceptConds? _) ¬p | dec-yes exp? a .proj₂ = refl - RATIFY-completeness s' (RATIFY-Continue (¬p , ¬a)) - rewrite dec-no (acceptConds? _) ¬p | dec-no exp? ¬a = refl - - completeness = cong (success {Err = ⊥}) ∘₂ RATIFY-completeness - -instance - Computational-RATIFY : Computational _⊢_⇀⦇_,RATIFY⦈_ ⊥ - Computational-RATIFY = record {Implementation} - -Computational-RATIFIES : Computational _⊢_⇀⦇_,RATIFIES⦈_ ⊥ -Computational-RATIFIES = it - -RATIFIES-total : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s' -RATIFIES-total = ReflexiveTransitiveClosure-total (Implementation.RATIFY-total _ _ _) - -RATIFIES-complete : ∀ {Γ s sig s'} → - Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s' → RATIFIES-total {Γ} {s} {sig} .proj₁ ≡ s' -RATIFIES-complete = computational⇒rightUnique Computational-RATIFIES (RATIFIES-total .proj₂) - -opaque - RATIFIES-total' : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s' - RATIFIES-total' = RATIFIES-total - - RATIFIES-complete' : ∀ {Γ s sig s'} → - Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s' → RATIFIES-total' {Γ} {s} {sig} .proj₁ ≡ s' - RATIFIES-complete' = RATIFIES-complete - - RATIFIES-deterministic : ∀ {Γ s sig s' s''} - → Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s' - → Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s'' - → s' ≡ s'' - RATIFIES-deterministic p₁ p₂ = trans (sym (RATIFIES-complete' p₁)) (RATIFIES-complete' p₂) - - RATIFIES-deterministic-≡ : ∀ {Γ Γ' s s' sig sig' s'' s'''} - → Γ ≡ Γ' - → s ≡ s' - → sig ≡ sig' - → Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s'' - → Γ' ⊢ s' ⇀⦇ sig' ,RATIFIES⦈ s''' - → s'' ≡ s''' - RATIFIES-deterministic-≡ refl refl refl = RATIFIES-deterministic +open import Ledger.Conway.Specification.Ratify.Properties.Computational diff --git a/src/Ledger/Conway/Specification/Ratify/Properties/Computational.agda b/src/Ledger/Conway/Specification/Ratify/Properties/Computational.agda new file mode 100644 index 000000000..e6836c8ae --- /dev/null +++ b/src/Ledger/Conway/Specification/Ratify/Properties/Computational.agda @@ -0,0 +1,88 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +module Ledger.Conway.Specification.Ratify.Properties.Computational + (txs : _) (open TransactionStructure txs) where + +open import Ledger.Conway.Specification.Gov txs +open import Ledger.Conway.Specification.Enact govStructure +open import Ledger.Conway.Specification.Enact.Properties.Computational govStructure +open import Ledger.Conway.Specification.Ratify txs + +open Computational ⦃...⦄ hiding (computeProof; completeness) + +private + module Implementation + Γ (s : RatifyState) (sig : GovActionID × _) + (let gid , st = sig) + where + open RatifyState s + open RatifyEnv Γ; open GovActionState st + es' = compute ⟦ gid , treasury , currentEpoch ⟧ es action + acc? = accepted? Γ es st + exp? = expired? currentEpoch st + del? = delayed? (action .gaType) prevAction es delay + + opaque + acceptConds? : ∀ a → Dec (acceptConds Γ s a) + acceptConds? _ = Dec-× ⦃ ⁇ accepted? _ _ _ ⦄ + ⦃ Dec-× ⦃ Dec-→ ⦃ ⁇ delayed? _ _ _ _ ⦄ ⦄ ⦃ ⁇ Computational⇒Dec' ⦄ ⦄ .dec + + RATIFY-total : ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' + RATIFY-total + with acceptConds? sig | exp? + ... | yes p@(_ , _ , (_ , q)) | _ = -, RATIFY-Accept (p , q) + ... | no ¬p | no ¬a = -, RATIFY-Continue (¬p , ¬a) + ... | no ¬p | yes a = -, RATIFY-Reject (¬p , a) + + computeProof = success {Err = ⊥} RATIFY-total + + RATIFY-completeness : ∀ s' → Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' → RATIFY-total .proj₁ ≡ s' + RATIFY-completeness stʳ (RATIFY-Accept (p , a)) with acceptConds? sig + ... | no ¬h = ⊥-elim (¬h p) + ... | yes (_ , _ , _ , h) = cong (λ stᵉ → ⟦ stᵉ , _ , _ ⟧) $ computational⇒rightUnique Computational-ENACT h a + RATIFY-completeness s' (RATIFY-Reject (¬p , a)) + rewrite dec-no (acceptConds? _) ¬p | dec-yes exp? a .proj₂ = refl + RATIFY-completeness s' (RATIFY-Continue (¬p , ¬a)) + rewrite dec-no (acceptConds? _) ¬p | dec-no exp? ¬a = refl + + completeness = cong (success {Err = ⊥}) ∘₂ RATIFY-completeness + +instance + Computational-RATIFY : Computational _⊢_⇀⦇_,RATIFY⦈_ ⊥ + Computational-RATIFY = record {Implementation} + +Computational-RATIFIES : Computational _⊢_⇀⦇_,RATIFIES⦈_ ⊥ +Computational-RATIFIES = it + +RATIFIES-total : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s' +RATIFIES-total = ReflexiveTransitiveClosure-total (Implementation.RATIFY-total _ _ _) + +RATIFIES-complete : ∀ {Γ s sig s'} → + Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s' → RATIFIES-total {Γ} {s} {sig} .proj₁ ≡ s' +RATIFIES-complete = computational⇒rightUnique Computational-RATIFIES (RATIFIES-total .proj₂) + +opaque + RATIFIES-total' : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s' + RATIFIES-total' = RATIFIES-total + + RATIFIES-complete' : ∀ {Γ s sig s'} → + Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s' → RATIFIES-total' {Γ} {s} {sig} .proj₁ ≡ s' + RATIFIES-complete' = RATIFIES-complete + + RATIFIES-deterministic : ∀ {Γ s sig s' s''} + → Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s' + → Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s'' + → s' ≡ s'' + RATIFIES-deterministic p₁ p₂ = trans (sym (RATIFIES-complete' p₁)) (RATIFIES-complete' p₂) + + RATIFIES-deterministic-≡ : ∀ {Γ Γ' s s' sig sig' s'' s'''} + → Γ ≡ Γ' + → s ≡ s' + → sig ≡ sig' + → Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s'' + → Γ' ⊢ s' ⇀⦇ sig' ,RATIFIES⦈ s''' + → s'' ≡ s''' + RATIFIES-deterministic-≡ refl refl refl = RATIFIES-deterministic diff --git a/src/Ledger/Conway/Specification/RewardUpdate/Properties.agda b/src/Ledger/Conway/Specification/RewardUpdate/Properties.agda new file mode 100644 index 000000000..3e799f19a --- /dev/null +++ b/src/Ledger/Conway/Specification/RewardUpdate/Properties.agda @@ -0,0 +1,5 @@ +{-# OPTIONS --safe #-} + +module Ledger.Conway.Specification.RewardUpdate.Properties where + +open import Ledger.Conway.Specification.RewardUpdate.Properties.Computational diff --git a/src/Ledger/Conway/Specification/RewardUpdate/Properties.lagda.md b/src/Ledger/Conway/Specification/RewardUpdate/Properties/Computational.agda similarity index 96% rename from src/Ledger/Conway/Specification/RewardUpdate/Properties.lagda.md rename to src/Ledger/Conway/Specification/RewardUpdate/Properties/Computational.agda index 7246dc7e4..5eb43fb09 100644 --- a/src/Ledger/Conway/Specification/RewardUpdate/Properties.lagda.md +++ b/src/Ledger/Conway/Specification/RewardUpdate/Properties/Computational.agda @@ -1,10 +1,9 @@ -```agda {-# OPTIONS --safe #-} open import Ledger.Conway.Specification.Transaction using (TransactionStructure) open import Ledger.Conway.Specification.Abstract using (AbstractFunctions) -module Ledger.Conway.Specification.RewardUpdate.Properties +module Ledger.Conway.Specification.RewardUpdate.Properties.Computational (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where @@ -49,4 +48,3 @@ instance with recomputeProof ruStep | completeness _ _ _ _ ruStep ... | success _ | refl = refl -``` diff --git a/src/Ledger/Conway/Specification/Utxo/Properties.agda b/src/Ledger/Conway/Specification/Utxo/Properties.agda index 4695b7856..30a0617c0 100644 --- a/src/Ledger/Conway/Specification/Utxo/Properties.agda +++ b/src/Ledger/Conway/Specification/Utxo/Properties.agda @@ -2,8 +2,8 @@ module Ledger.Conway.Specification.Utxo.Properties where +open import Ledger.Conway.Specification.Utxo.Properties.Base open import Ledger.Conway.Specification.Utxo.Properties.Computational -open import Ledger.Conway.Specification.Utxo.Properties.DepositHelpers open import Ledger.Conway.Specification.Utxo.Properties.GenMinSpend open import Ledger.Conway.Specification.Utxo.Properties.MinSpend open import Ledger.Conway.Specification.Utxo.Properties.PoV diff --git a/src/Ledger/Conway/Specification/Utxo/Properties/DepositHelpers.agda b/src/Ledger/Conway/Specification/Utxo/Properties/Base.agda similarity index 98% rename from src/Ledger/Conway/Specification/Utxo/Properties/DepositHelpers.agda rename to src/Ledger/Conway/Specification/Utxo/Properties/Base.agda index 00a49f9e6..d5ab7c6c7 100644 --- a/src/Ledger/Conway/Specification/Utxo/Properties/DepositHelpers.agda +++ b/src/Ledger/Conway/Specification/Utxo/Properties/Base.agda @@ -3,7 +3,7 @@ open import Ledger.Conway.Specification.Abstract open import Ledger.Conway.Specification.Transaction -module Ledger.Conway.Specification.Utxo.Properties.DepositHelpers +module Ledger.Conway.Specification.Utxo.Properties.Base (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where @@ -227,9 +227,6 @@ module _ ℤ.+_ uDep + (dep - uDep) ≡⟨ Int.distribʳ-⊖-+-pos uDep dep uDep ⟩ (uDep + dep) - uDep ≡⟨ cong (_- uDep) (+-comm uDep dep) ⟩ (dep + uDep) - uDep ≡˘⟨ Int.distribʳ-⊖-+-pos dep uDep uDep ⟩ - -- ℤ.+_ uDep + (dep - uDep) ≡⟨ distribʳ-⊖-+-pos uDep dep uDep ⟩ - -- (uDep + dep) - uDep ≡⟨ cong (_- uDep) (+-comm uDep dep) ⟩ - -- (dep + uDep) - uDep ≡˘⟨ distribʳ-⊖-+-pos dep uDep uDep ⟩ ℤ.+_ dep ℤ.+ (uDep - uDep) ≡⟨ cong (λ u → ℤ.+_ dep ℤ.+ u) (n⊖n≡0 uDep) ⟩ ℤ.+_ dep ℤ.+ ℤ.0ℤ ≡⟨ Int.+-identityʳ _ ⟩ ℤ.+_ dep ∎ diff --git a/src/Ledger/Conway/Specification/Utxo/Properties/Computational.lagda b/src/Ledger/Conway/Specification/Utxo/Properties/Computational.agda similarity index 93% rename from src/Ledger/Conway/Specification/Utxo/Properties/Computational.lagda rename to src/Ledger/Conway/Specification/Utxo/Properties/Computational.agda index ad329ad4c..006131b53 100644 --- a/src/Ledger/Conway/Specification/Utxo/Properties/Computational.lagda +++ b/src/Ledger/Conway/Specification/Utxo/Properties/Computational.agda @@ -1,7 +1,3 @@ -\subsection{UTxO} -\label{sec:utxo-properties} - -\begin{code}[hide] {-# OPTIONS --safe #-} open import Ledger.Conway.Specification.Abstract @@ -136,27 +132,13 @@ opaque Computational-UTXO = Computational-UTXO' private variable - tx : Tx - utxo utxo' : UTxO - Γ : UTxOEnv - utxoState utxoState' : UTxOState - fees fees' : Fees - donations donations' : Donations - deposits deposits' : Deposits - -\end{code} + tx : Tx + Γ : UTxOEnv + utxoState utxoState' : UTxOState -Here we state the fact that the UTxO relation is computable. - -\begin{figure*}[h] -\begin{code} UTXO-step : UTxOEnv → UTxOState → Tx → ComputationResult String UTxOState UTXO-step = compute ⦃ Computational-UTXO ⦄ UTXO-step-computes-UTXO : UTXO-step Γ utxoState tx ≡ success utxoState' ⇔ Γ ⊢ utxoState ⇀⦇ tx ,UTXO⦈ utxoState' UTXO-step-computes-UTXO = ≡-success⇔STS ⦃ Computational-UTXO ⦄ -\end{code} -\caption{Computing the UTXO transition system} -\end{figure*} - diff --git a/src/Ledger/Conway/Specification/Utxo/Properties/PoV.lagda.md b/src/Ledger/Conway/Specification/Utxo/Properties/PoV.lagda.md index 775064f8a..d89cbc7b5 100644 --- a/src/Ledger/Conway/Specification/Utxo/Properties/PoV.lagda.md +++ b/src/Ledger/Conway/Specification/Utxo/Properties/PoV.lagda.md @@ -14,7 +14,7 @@ module Ledger.Conway.Specification.Utxo.Properties.PoV open import Ledger.Conway.Specification.Certs govStructure open import Ledger.Prelude open import Ledger.Conway.Specification.Utxo txs abs -open import Ledger.Conway.Specification.Utxo.Properties.DepositHelpers txs abs public +open import Ledger.Conway.Specification.Utxo.Properties.Base txs abs public open UTxOState; open Tx; open TxBody ``` --> diff --git a/src/Ledger/Conway/Specification/Utxow/Properties.agda b/src/Ledger/Conway/Specification/Utxow/Properties.agda new file mode 100644 index 000000000..e55c227c8 --- /dev/null +++ b/src/Ledger/Conway/Specification/Utxow/Properties.agda @@ -0,0 +1,5 @@ +{-# OPTIONS --safe #-} + +module Ledger.Conway.Specification.Utxow.Properties where + +open import Ledger.Conway.Specification.Utxow.Properties.Computational From 07fe940fcacb994e48b3eae3f2de7e60328085f6 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 29 Sep 2025 15:43:34 -0600 Subject: [PATCH 6/6] cleanup Specification module --- src/Ledger/Conway/Specification.agda | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) diff --git a/src/Ledger/Conway/Specification.agda b/src/Ledger/Conway/Specification.agda index e69af55f2..1f94d46d9 100644 --- a/src/Ledger/Conway/Specification.agda +++ b/src/Ledger/Conway/Specification.agda @@ -1,24 +1,16 @@ {-# OPTIONS --safe #-} module Ledger.Conway.Specification where +import Ledger.Conway.Specification.BlockBody +import Ledger.Conway.Specification.BlockBody.Properties import Ledger.Conway.Specification.Certs import Ledger.Conway.Specification.Certs.Properties -import Ledger.Conway.Specification.Certs.Properties.PoV -import Ledger.Conway.Specification.Certs.Properties.PoVLemmas -import Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg import Ledger.Conway.Specification.Chain import Ledger.Conway.Specification.Chain.Properties -import Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds -import Ledger.Conway.Specification.Chain.Properties.EpochStep -import Ledger.Conway.Specification.Chain.Properties.GovDepsMatch -import Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed import Ledger.Conway.Specification.Enact import Ledger.Conway.Specification.Enact.Properties import Ledger.Conway.Specification.Epoch import Ledger.Conway.Specification.Epoch.Properties -import Ledger.Conway.Specification.Epoch.Properties.ConstRwds -import Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch -import Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps import Ledger.Conway.Specification.Fees import Ledger.Conway.Specification.Gov import Ledger.Conway.Specification.Gov.Actions @@ -26,13 +18,13 @@ import Ledger.Conway.Specification.Gov.Properties import Ledger.Conway.Specification.Gov.Properties.ChangePPGroup import Ledger.Conway.Specification.Ledger import Ledger.Conway.Specification.Ledger.Properties -import Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch -import Ledger.Conway.Specification.Ledger.Properties.PoV import Ledger.Conway.Specification.PParams import Ledger.Conway.Specification.Properties import Ledger.Conway.Specification.Ratify import Ledger.Conway.Specification.Ratify.Properties import Ledger.Conway.Specification.Rewards +import Ledger.Conway.Specification.RewardUpdate +import Ledger.Conway.Specification.RewardUpdate.Properties import Ledger.Conway.Specification.Script import Ledger.Conway.Specification.Script.Validation import Ledger.Conway.Specification.Test.Examples @@ -45,7 +37,5 @@ import Ledger.Conway.Specification.Transaction import Ledger.Conway.Specification.Types.GovStructure import Ledger.Conway.Specification.Utxo import Ledger.Conway.Specification.Utxo.Properties -import Ledger.Conway.Specification.Utxo.Properties.MinSpend -import Ledger.Conway.Specification.Utxo.Properties.PoV import Ledger.Conway.Specification.Utxow import Ledger.Conway.Specification.Utxow.Properties