PoV

{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction

module Ledger.Conway.Specification.Utxo.Properties.PoV
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs)
  where

open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Prelude
open import Ledger.Conway.Specification.Utxo txs abs
open import Ledger.Conway.Specification.Utxo.Properties txs abs using (χ; module DepositHelpers)
open UTxOState; open Tx; open TxBody

Lemma (The UTXO rule preserves value).

Informally.

Let s and s' be UTxOStates, let tx : Tx be a fresh transaction with withdrawals txwdrls, and suppose s ⇀⦇ tx ,UTXO⦈ s'. If tx is valid. Then the coin value of s' is equal to the sum of the coin values of s and txwdrls. If tx is not valid, then the coin values of s and s' are equal. We can express this concisely as follows:

getCoin s + getCoin (wdrlsOf tx) * χ (tx .isValid) ≡ getCoin s'

where χ : Bool → \(\{0, 1\}\) is the characteristic function, which returns 0 for false and 1 for true.

Formally.

UTXOpov : {Γ : UTxOEnv} {tx : Tx} {s s' : UTxOState}
  → txidOf tx ∉ mapˢ proj₁ (dom (UTxOOf s))
  → Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
  → getCoin s + getCoin (wdrlsOf tx) * χ (tx .isValid) ≡ getCoin s'

Proof.

UTXOpov h' step@(UTXO-inductive⋯ _ Γ _ _ _ _ _ _ _ newBal noMintAda _ _ _ _ _ _ _ _ _ (Scripts-Yes (_ , _ , valid)))
  = DepositHelpers.pov-scripts step h' refl valid

UTXOpov h' step@(UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (Scripts-No (_ , invalid)))
  = DepositHelpers.pov-no-scripts step h' invalid