PoV

{-# OPTIONS --safe #-}

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

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

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

- *Informally*. Let and be `UTxOState`{.AgdaRecord}s, let : `Tx`{.AgdaRecord} be a fresh transaction with withdrawals , and suppose `⇀⦇`{.AgdaDatatype} `,UTXO⦈`{.AgdaDatatype} . If is valid, then the coin value of is equal to the sum of the coin values of and . If is not valid, then the coin values of and are equal. We can express this concisely as follows: where $χ : \texttt{@@AgdaTerm@@basename=Bool@@class=AgdaDatatype@@} → {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*. See the module in the [formal ledger repository](\repourl).

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