PoV
Theorem (The LEDGER
rule preserves value).
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.
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 txWithdrawals)) 0 in begin getCoin utxoSt + getCoin certState ≡⟨ cong (getCoin utxoSt +_) (CERTS-pov 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 ⟩ 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#3104}{\htmlId{4969}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{4976}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{4983}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{4994}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ ≡˘⟨ +-identityʳ (getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5041}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5048}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5055}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5066}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$) ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5097}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5104}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5111}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5122}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + 0 ≡˘⟨ cong (getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5166}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5173}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5180}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5191}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ +_) (*-zeroʳ (getCoin txWithdrawals)) ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5259}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5266}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5273}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5284}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txWithdrawals * 0 ≡˘⟨ cong (λ x → getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5358}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5365}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5372}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5383}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txWithdrawals * χ x) invalid ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5452}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5459}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5466}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5477}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txWithdrawals * χ isValid ≡⟨ UTXOpov h st ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4791}{\htmlId{5567}{\htmlClass{Function}{\text{utxo'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4806}{\htmlId{5575}{\htmlClass{Function}{\text{fees'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4866}{\htmlId{5583}{\htmlClass{Function}{\text{deposits'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4890}{\htmlId{5595}{\htmlClass{Function}{\text{donations'}}}}\, \end{pmatrix}$ ∎ ) where open ≡-Reasoning