PoV
Theorem: The LEDGER rule preserves value¶
{-# OPTIONS --safe #-} open import Ledger.Conway.Specification.Transaction open import Ledger.Conway.Specification.Abstract module Ledger.Conway.Specification.Ledger.Properties.PoV (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where open import Ledger.Conway.Specification.Certs govStructure open import Ledger.Conway.Specification.Chain txs abs open import Ledger.Conway.Specification.Certs.Properties.Computational 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.PoV txs abs open import Ledger.Conway.Specification.Utxow txs abs open import Axiom.Set.Properties th open import Data.Nat.Properties using (+-0-monoid; +-identityʳ; +-comm; +-assoc; *-identityʳ; *-zeroʳ) instance HasCoin-LState : HasCoin LState HasCoin-LState .getCoin s = getCoin (LState.utxoSt s) + getCoin (LState.certState s) module _ (tx : Tx) (let open Tx tx; open TxBody body) ( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) → disjoint (dom m) (dom m') → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' ) ( 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 ) where pattern UTXO-induction r = UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ r _ _ _
Informally.
Let s and s' be ledger states and
let tx : Tx be a fresh transaction, that is, a transaction
that is not already part of the UTxOState of s. If
s ⇀⦇ tx ,LEDGER⦈ s',
then the coin values of s and s' are equal, that is,
getCoin s \(≡\) getCoin s'.
Formally.
LEDGER-pov : {Γ : LEnv} {s s' : LState} → txId ∉ mapˢ proj₁ (dom (UTxOOf s)) → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → getCoin s ≡ getCoin s'
Proof. (Click the "Show more Agda" button to reveal the formal proof.)
LEDGER-pov {s = s} {s' = s'} h (LEDGER-V {utxoSt' = utxoSt''} ( valid , UTXOW⇒UTXO st@(UTXO-induction r) , h' , _ )) = let open LState s open CertState certState open LState s' renaming (utxoSt to utxoSt'; govSt to govSt'; certState to certState') open CertState certState' open ≡-Reasoning open Certs-PoV indexedSumᵛ'-∪ sumConstZero res-decomp getCoin-cong ≡ᵉ-getCoinˢ zeroMap = constMap (mapˢ RewardAddress.stake (dom txWithdrawals)) 0 in begin getCoin utxoSt + getCoin certState ≡⟨ cong (getCoin utxoSt +_) (CERTS-pov r h') ⟩ getCoin utxoSt + (getCoin certState' + getCoin txWithdrawals) ≡˘⟨ 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) ≡⟨ cong (getCoin utxoSt +_) (+-comm (getCoin certState') _) ⟩ getCoin utxoSt + (getCoin txWithdrawals * χ isValid + getCoin certState') ≡˘⟨ +-assoc (getCoin utxoSt) (getCoin txWithdrawals * χ isValid) (getCoin certState') ⟩ getCoin utxoSt + getCoin txWithdrawals * χ isValid + getCoin certState' ≡⟨ cong (_+ getCoin certState') (UTXOpov h st) ⟩ getCoin utxoSt' + getCoin certState' ∎ LEDGER-pov {s = s} {s' = s'} h (LEDGER-I {utxoSt' = utxoSt''} (invalid , UTXOW⇒UTXO st)) = let open LState s open CertState certState open LState s' renaming (utxoSt to utxoSt'; govSt to govSt'; certState to certState') open UTxOState utxoSt open UTxOState utxoSt' renaming (utxo to utxo'; fees to fees' ; deposits to deposits'; donations to donations') in cong (_+ rewardsBalance dState) ( begin getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#2998}{\htmlId{5011}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3020}{\htmlId{5018}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3042}{\htmlId{5025}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3068}{\htmlId{5036}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ ≡˘⟨ +-identityʳ (getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#2998}{\htmlId{5083}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3020}{\htmlId{5090}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3042}{\htmlId{5097}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3068}{\htmlId{5108}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$) ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#2998}{\htmlId{5139}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3020}{\htmlId{5146}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3042}{\htmlId{5153}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3068}{\htmlId{5164}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + 0 ≡˘⟨ cong (getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#2998}{\htmlId{5208}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3020}{\htmlId{5215}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3042}{\htmlId{5222}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3068}{\htmlId{5233}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ +_) (*-zeroʳ (getCoin txWithdrawals)) ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#2998}{\htmlId{5301}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3020}{\htmlId{5308}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3042}{\htmlId{5315}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3068}{\htmlId{5326}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txWithdrawals * 0 ≡˘⟨ cong (λ x → getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#2998}{\htmlId{5400}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3020}{\htmlId{5407}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3042}{\htmlId{5414}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3068}{\htmlId{5425}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txWithdrawals * χ x) invalid ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#2998}{\htmlId{5494}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3020}{\htmlId{5501}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3042}{\htmlId{5508}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3068}{\htmlId{5519}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txWithdrawals * χ isValid ≡⟨ UTXOpov h st ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4833}{\htmlId{5609}{\htmlClass{Function}{\text{utxo'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4848}{\htmlId{5617}{\htmlClass{Function}{\text{fees'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4908}{\htmlId{5625}{\htmlClass{Function}{\text{deposits'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4932}{\htmlId{5637}{\htmlClass{Function}{\text{donations'}}}}\, \end{pmatrix}$ ∎ ) where open ≡-Reasoning