Specification: Transactions

This document provides a partial specification of the Tx type and related types, as needed by the Deposit Wallet.

module Specification.Cardano.Tx where

A Tx represents a transaction. A transactions creates transaction outputs and spends previously created transaction outputs.

Imports

open import Haskell.Prelude
open import Haskell.Reasoning

Signature

A signature records data types, operations, and the properties that these operations should satisfy.

record Signature (Address : Set) (Value : Set) : Set₁ where
  field

We are concerned with types

    TxBody : Set
    Tx     : Set
    TxId   : Set

that support the following operations:

    outputs : TxBody → List (Address × Value)
    getTxId : Tx → TxId