Skip to content

Symbolic Transaction

Overview

In this section, we define data types and validation logic of a Symbolic Transaction.

Data Types

In addition to the data types introduced at the ledger level, we define the types related to the transaction validation.

Basic types

  1. Int128 is a \(128\)-bit signed integer.

Symbolic Transaction types

  1. Datum is a wrapper around F.
  2. AssetValue is a record type with the following fields:
    1. assetPolicy is of type Address. It is the address of the initial UTxO that contains the token.
    2. assetName is a wrapper around type F. It is the datum of the initial UTxO that contains the token.
    3. assetQuantity is of type Int128.
  3. Value is a list [AssetValue].
  4. Output is a record type with the following fields:
    1. txoAddress is of type Address. It is the address of the output.
    2. txoValue is of type Value. It is the value in the output.
    3. txoDatum is of type Datum. It is the extra input to the output's spending condition.
  5. InputRef is a record type with the following fields:
    1. refTxId is of type Hash Transaction. It is the hash of the transaction that produced this output.
    2. refTxIdx is a wrapper around F. It is the index of the output in the list of outputs of the transaction that produced this output.
  6. Input is a record type with the following fields:
    1. txiReference is of type InputRef. It is the reference to the output being spent.
    2. txiOutput is of type Output. It is the contents of the output being spent.
  7. Transaction is a record type with the following fields:
    1. [Input] : list of inputs of the transaction.
    2. [Output] : list of outputs of the transaction.
  8. TransactionWitness is the supplemental data used in the transaction validation (see below).

UTxO set

Transaction outputs can be used to describe the state of the ledger. When a valid transaction is applied to the ledger, its outputs are added to the active UTxO set which is a set of all unspent transaction outputs. When an output becomes spent, it is removed from the set.

In order for an output to be considered spent, the following conditions must be met:

  1. A valid transaction that contains the output among its inputs must be applied to the ledger.
  2. The address on the envelope must be the same as the address of the output.

Other transaction inputs are called reference inputs. They influence transaction validation but are not considered spent.

Validation rules

We now describe the Symbolic Transaction validation rules.

The transaction validation function has the following signature:

validateTx :: F -> TransactionBatch -> TransactionEnvelope -> TransactionWitness -> (F, F)

Transaction validation proceeds as follows:

  1. Decode the first argument as Hash Value (using TransactionWitness data).
  2. Decode txeTransactionId field of TransactionEnvelope as Hash Transaction (using TransactionWitness data).

  3. Check that every transaction input is in the active UTxO set:

    a. It must be produced by some transaction from an earlier transaction batch or bridged in from the underlying blockchain.

    b. It must not be spent in any transaction batch between its creation and the current batch.

  4. Check that there is at least one transaction input corresponding to the envelope's address.

  5. Check that the circuit corresponding to the envelope's address outputs 0.
  6. Check that all outputs contain non-negative value.
  7. If checks 3-6 are successful, we set the first output to 0. Otherwise, we set it to a non-zero value.

  8. Calculate the multi-asset value difference between the inputs (at the envelope's address) and the outputs, exclude the value of the asset policy associated with the address, hash it, and return as the second output. To this difference, we add decoded first argument and set it as second output of this function.

    Note

    An address \(A\) can mint and burn tokens of policy \(A\). The circuit that locks outputs at the address is used as a minting policy.