PoV
Theorem (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{4965}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{4972}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{4979}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{4990}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ ≡˘⟨ +-identityʳ (getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5037}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5044}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5051}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5062}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$) ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5093}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5100}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5107}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5118}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + 0 ≡˘⟨ cong (getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5162}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5169}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5176}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5187}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ +_) (*-zeroʳ (getCoin txWithdrawals)) ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5255}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5262}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5269}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5280}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txWithdrawals * 0 ≡˘⟨ cong (λ x → getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5354}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5361}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5368}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5379}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txWithdrawals * χ x) invalid ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5448}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5455}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5462}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5473}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txWithdrawals * χ isValid ≡⟨ UTXOpov h st ⟩ getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4787}{\htmlId{5563}{\htmlClass{Function}{\text{utxo'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4802}{\htmlId{5571}{\htmlClass{Function}{\text{fees'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4862}{\htmlId{5579}{\htmlClass{Function}{\text{deposits'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4886}{\htmlId{5591}{\htmlClass{Function}{\text{donations'}}}}\, \end{pmatrix}$ ∎ ) where open ≡-Reasoning