PoV

{-# 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ʳ)

-- ** 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 _ _ _

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 Certs-PoV 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 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#3104}{\htmlId{4868}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{4875}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{4882}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{4893}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$
        ≡˘⟨ +-identityʳ (getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{4940}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{4947}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{4954}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{4965}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$) ⟩
      getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{4996}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5003}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5010}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5021}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + 0
        ≡˘⟨ cong (getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5065}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5072}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5079}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5090}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ +_) (*-zeroʳ (getCoin txWithdrawals)) ⟩
      getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5158}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5165}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5172}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5183}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txWithdrawals * 0
        ≡˘⟨ cong (λ x → getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5257}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5264}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5271}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5282}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txWithdrawals * χ x) invalid ⟩
      getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{5351}{\htmlClass{Function}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{5358}{\htmlClass{Function}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{5365}{\htmlClass{Function}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#3174}{\htmlId{5376}{\htmlClass{Function}{\text{donations}}}}\, \end{pmatrix}$ + getCoin txWithdrawals * χ isValid
        ≡⟨ UTXOpov h st ⟩
      getCoin $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4690}{\htmlId{5466}{\htmlClass{Function}{\text{utxo'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4705}{\htmlId{5474}{\htmlClass{Function}{\text{fees'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4765}{\htmlId{5482}{\htmlClass{Function}{\text{deposits'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.Properties.PoV.html#4789}{\htmlId{5494}{\htmlClass{Function}{\text{donations'}}}}\, \end{pmatrix}$ ∎ )
    where open ≡-Reasoning