PoV
{-# OPTIONS --safe #-} open import Ledger.Conway.Transaction open import Ledger.Conway.Abstract module Ledger.Conway.Ledger.Properties.PoV (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where
open import Ledger.Conway.Certs govStructure open import Ledger.Conway.Chain txs abs open import Ledger.Conway.Certs.Properties govStructure open import Ledger.Conway.Ledger txs abs open import Ledger.Prelude open import Ledger.Conway.Utxo txs abs open import Ledger.Conway.Utxo.Properties txs abs using (χ; module DepositHelpers) open import Ledger.Conway.Utxo.Properties.PoV txs abs open import Ledger.Conway.Utxow txs abs open import Axiom.Set.Properties th open import Data.Nat.Properties using (+-0-monoid; +-identityʳ; +-comm; +-assoc; *-identityʳ; *-zeroʳ) -- ** Proof that LEDGER preserves values. 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 , : `LState`{.AgdaRecord} be ledger states and let :
`Tx`{.AgdaRecord} be a *fresh* transaction, that is, a transaction
that is not already part of the `UTxOState`{.AgdaRecord} of . If
`⇀⦇`{.AgdaDatatype} `,LEDGER⦈`{.AgdaDatatype} , then the coin values
of and are equal, that is, `getCoin`{.AgdaField} $≡$
`getCoin`{.AgdaField} .
- *Formally*.
LEDGER-pov : {Γ : LEnv} {s s' : LState} → txid ∉ mapˢ proj₁ (dom (UTxOOf s)) → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → getCoin s ≡ getCoin s'- *Proof*. See the module in the [formal ledger repository](\repourl).
-- 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 CERTSpov indexedSumᵛ'-∪ sumConstZero res-decomp getCoin-cong ≡ᵉ-getCoinˢ r zeroMap = constMap (mapˢ RwdAddr.stake (dom txwdrls)) 0 in begin getCoin utxoSt + getCoin certState ≡⟨ cong (getCoin utxoSt +_) (CERTS-pov h') ⟩ getCoin utxoSt + (getCoin certState' + getCoin txwdrls) ≡˘⟨ cong (λ x → getCoin utxoSt + (getCoin certState' + x )) (*-identityʳ (getCoin txwdrls)) ⟩ -- cong (λ u → getCoin utxoSt + (getCoin certState' + getCoin txwdrls * χ u)) valid ⟩ getCoin utxoSt + (getCoin certState' + getCoin txwdrls * 1) ≡˘⟨ cong (λ u → getCoin utxoSt + (getCoin certState' + getCoin txwdrls * χ u)) valid ⟩ getCoin utxoSt + (getCoin certState' + getCoin txwdrls * χ isValid) ≡⟨ cong (getCoin utxoSt +_) (+-comm (getCoin certState') _) ⟩ getCoin utxoSt + (getCoin txwdrls * χ isValid + getCoin certState') ≡˘⟨ +-assoc (getCoin utxoSt) (getCoin txwdrls * χ isValid) (getCoin certState') ⟩ getCoin utxoSt + getCoin txwdrls * χ 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.Utxo.html#4779}{\htmlId{4706}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4801}{\htmlId{4713}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4823}{\htmlId{4720}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4849}{\htmlId{4731}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ ≡˘⟨ +-identityʳ (getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Utxo.html#4779}{\htmlId{4778}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4801}{\htmlId{4785}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4823}{\htmlId{4792}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4849}{\htmlId{4803}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$) ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Utxo.html#4779}{\htmlId{4834}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4801}{\htmlId{4841}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4823}{\htmlId{4848}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4849}{\htmlId{4859}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + 0 ≡˘⟨ cong (getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Utxo.html#4779}{\htmlId{4903}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4801}{\htmlId{4910}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4823}{\htmlId{4917}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4849}{\htmlId{4928}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ +_) (*-zeroʳ (getCoin txwdrls)) ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Utxo.html#4779}{\htmlId{4990}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4801}{\htmlId{4997}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4823}{\htmlId{5004}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4849}{\htmlId{5015}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txwdrls * 0 ≡˘⟨ cong (λ x → getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Utxo.html#4779}{\htmlId{5083}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4801}{\htmlId{5090}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4823}{\htmlId{5097}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4849}{\htmlId{5108}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txwdrls * χ x) invalid ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Utxo.html#4779}{\htmlId{5171}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4801}{\htmlId{5178}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4823}{\htmlId{5185}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#4849}{\htmlId{5196}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txwdrls * χ isValid ≡⟨ UTXOpov h st ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Ledger.Properties.PoV.html#4528}{\htmlId{5280}{\htmlClass{Function}{\text{utxo'}}}}\, \\ \,\href{Ledger.Conway.Ledger.Properties.PoV.html#4543}{\htmlId{5288}{\htmlClass{Function}{\text{fees'}}}}\, \\ \,\href{Ledger.Conway.Ledger.Properties.PoV.html#4603}{\htmlId{5296}{\htmlClass{Function}{\text{deposits'}}}}\, \\ \,\href{Ledger.Conway.Ledger.Properties.PoV.html#4627}{\htmlId{5308}{\htmlClass{Function}{\text{donations'}}}}\, \end{pmatrix}$ ∎ ) where open ≡-Reasoning