Transactions¶

This section is part of the Ledger.Conway.Transaction module of the formal ledger specification, where we define transactions.

A transaction consists of a transaction body, a collection of witnesses and some optional auxiliary data.

{-# OPTIONS --safe #-}
--------------------------------------------------------------------------------
-- NOTE: Everything in this module is part of TransactionStructure
--------------------------------------------------------------------------------
module Ledger.Conway.Transaction where

import Data.Maybe.Base as M

open import Ledger.Prelude renaming (filterᵐ to filter)

open import Ledger.Conway.Crypto
open import Ledger.Conway.Types.Epoch
open import Ledger.Conway.Gov.Base
import Ledger.Conway.PParams
import Ledger.Conway.Script.Base
import Ledger.Conway.Gov.Actions
import Ledger.Conway.Certs
import Ledger.Conway.TokenAlgebra.Base
import Ledger.Conway.Address

open import Relation.Nullary.Decidable using (⌊_⌋)

data Tag : Type where
  Spend Mint Cert Rewrd Vote Propose : Tag
unquoteDecl DecEq-Tag = derive-DecEq ((quote Tag , DecEq-Tag) ∷ [])

Some key ingredients in the transaction body are:

A set txins of transaction inputs, each of which identifies an output from a previous transaction. A transaction input consists of a transaction id and an index to uniquely identify the output.
An indexed collection txouts of transaction outputs. The TxOut type is an address paired with a coin value.
A transaction fee. This value will be added to the fee pot.
The hash txid of the serialized form of the transaction that was included in the block.

Conway specifics

Ingredients of the transaction body introduced in the Conway era are the following:

txvote, the list of votes for goverance actions;
txprop, the list of governance proposals;
txdonation, amount of Coin to donate to treasury, e.g., to return money to the treasury after a governance action;
curTreasury, the current value of the treasury. This field serves as a precondition to executing Plutus scripts that access the value of the treasury.

record TransactionStructure : Type₁ where
  field

Abstract types

    Ix TxId AuxiliaryData : Type

    ⦃ DecEq-Ix   ⦄ : DecEq Ix
    ⦃ DecEq-TxId ⦄ : DecEq TxId
    adHashingScheme : isHashableSet AuxiliaryData
  open isHashableSet adHashingScheme renaming (THash to ADHash) public

  field globalConstants : _
  open GlobalConstants globalConstants public

  field crypto : _
  open Crypto crypto public
  open Ledger.Conway.TokenAlgebra.Base ScriptHash public
  open Ledger.Conway.Address Network KeyHash ScriptHash ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ public

  field epochStructure : _
  open EpochStructure epochStructure public
  open Ledger.Conway.Script.Base crypto epochStructure public

  field scriptStructure : _
  open ScriptStructure scriptStructure public
  open Ledger.Conway.PParams crypto epochStructure scriptStructure public

  field govParams : _
  open GovParams govParams public

  field tokenAlgebra : TokenAlgebra
  open TokenAlgebra tokenAlgebra public

  field txidBytes : TxId → Ser

  govStructure : GovStructure
  govStructure = record
    -- TODO: figure out what to do with the hash
    { TxId = TxId; DocHash = ADHash
    ; crypto = crypto
    ; epochStructure = epochStructure
    ; scriptStructure = scriptStructure
    ; govParams = govParams
    ; globalConstants = globalConstants
    }

  module GovActions = Ledger.Conway.Gov.Actions govStructure
  open GovActions hiding (Vote; yes; no; abstain) public

  open import Ledger.Conway.Certs govStructure

Derived types

  TxIn     = TxId × Ix
  TxOut    = Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe Script
  UTxO     = TxIn ⇀ TxOut
  Wdrl     = RwdAddr ⇀ Coin
  RdmrPtr  = Tag × Ix

  ProposedPPUpdates  = KeyHash ⇀ PParamsUpdate
  Update             = ProposedPPUpdates × Epoch

  record HasUTxO {a} (A : Type a) : Type a where
    field UTxOOf : A → UTxO
  open HasUTxO ⦃...⦄ public

Transaction types

  record TxBody : Type where
    field
      txins          : ℙ TxIn
      refInputs      : ℙ TxIn
      txouts         : Ix ⇀ TxOut
      txfee          : Coin
      mint           : Value
      txvldt         : Maybe Slot × Maybe Slot
      txcerts        : List DCert
      txwdrls        : Wdrl
      txvote         : List GovVote
      txprop         : List GovProposal
      txdonation     : Coin
      txup           : Maybe Update
      txADhash       : Maybe ADHash
      txNetworkId    : Maybe Network
      curTreasury    : Maybe Coin
      txid           : TxId
      collateral     : ℙ TxIn
      reqSigHash     : ℙ KeyHash
      scriptIntHash  : Maybe ScriptHash

  record HasTxBody {a} (A : Type a) : Type a where
    field TxBodyOf : A → TxBody
  open HasTxBody  ⦃...⦄ public

  record Hastxfee {a} (A : Type a) : Type a where
    field txfeeOf : A → Coin
  open Hastxfee   ⦃...⦄ public

  record Hastxcerts {a} (A : Type a) : Type a where
    field txcertsOf : A → List DCert
  open Hastxcerts ⦃...⦄ public

  record Hastxprop {a} (A : Type a) : Type a where
    field txpropOf  : A → List GovProposal
  open Hastxprop  ⦃...⦄ public

  record Hastxid    {a} (A : Type a) : Type a where
    field txidOf    : A → TxId
  open Hastxid    ⦃...⦄ public

  record TxWitnesses : Type where
    field
      vkSigs   : VKey ⇀ Sig
      scripts  : ℙ Script
      txdats   : ℙ Datum
      txrdmrs  : RdmrPtr  ⇀ Redeemer × ExUnits

    scriptsP1 : ℙ P1Script
    scriptsP1 = mapPartial toP1Script scripts

  record Tx : Type where
    field
      body     : TxBody
      wits     : TxWitnesses
      txsize   : ℕ
      isValid  : Bool
      txAD     : Maybe AuxiliaryData

  instance
    HasTxBody-Tx : HasTxBody Tx
    HasTxBody-Tx .TxBodyOf = Tx.body

    Hastxfee-Tx : Hastxfee Tx
    Hastxfee-Tx .txfeeOf = TxBody.txfee ∘ TxBodyOf

    Hastxcerts-Tx : Hastxcerts Tx
    Hastxcerts-Tx .txcertsOf = TxBody.txcerts ∘ TxBodyOf

    Hastxprop-Tx : Hastxprop Tx
    Hastxprop-Tx .txpropOf = TxBody.txprop ∘ TxBodyOf

    HasWdrls-TxBody : HasWdrls TxBody
    HasWdrls-TxBody .wdrlsOf = TxBody.txwdrls

    HasWdrls-Tx : HasWdrls Tx
    HasWdrls-Tx .wdrlsOf = wdrlsOf ∘ TxBodyOf

    Hastxid-Tx : Hastxid Tx
    Hastxid-Tx .txidOf = TxBody.txid ∘ TxBodyOf

  getValue : TxOut → Value
  getValue (_ , v , _) = v

  TxOutʰ = Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe ScriptHash

  txOutHash : TxOut → TxOutʰ
  txOutHash (a , v , d , s) = a , (v , (d , M.map hash s))

  getValueʰ : TxOutʰ → Value
  getValueʰ (_ , v , _) = v

  txinsVKey : ℙ TxIn → UTxO → ℙ TxIn
  txinsVKey txins utxo = txins ∩ dom (utxo ∣^' (isVKeyAddr ∘ proj₁))

  scriptOuts : UTxO → UTxO
  scriptOuts utxo = filter (λ (_ , addr , _) → isScriptAddr addr) utxo

  txinsScript : ℙ TxIn → UTxO → ℙ TxIn
  txinsScript txins utxo = txins ∩ dom (proj₁ (scriptOuts utxo))

  refScripts : Tx → UTxO → ℙ Script
  refScripts tx utxo =
    mapPartial (proj₂ ∘ proj₂ ∘ proj₂) (range (utxo ∣ (txins ∪ refInputs)))
    where open Tx; open TxBody (tx .body)

  txscripts : Tx → UTxO → ℙ Script
  txscripts tx utxo = scripts (tx .wits) ∪ refScripts tx utxo
    where open Tx; open TxWitnesses

  lookupScriptHash : ScriptHash → Tx → UTxO → Maybe Script
  lookupScriptHash sh tx utxo = lookupᵐ? m sh
    where m = setToMap (mapˢ < hash , id > (txscripts tx utxo))

  instance
    HasCoin-TxOut : HasCoin TxOut
    HasCoin-TxOut .getCoin = coin ∘ proj₁ ∘ proj₂

Transactions¶

Transactions and related types¶

Functions related to transactions¶