Skip to content

Symbolic Ledger

Overview

In this section, we define data types and validation logic of the Symbolic Ledger.

Data Types

Basic types

  1. F is a field element.
  2. Bool is a boolean type.
  3. POSIXTime is a datetime in POSIX format.
  4. Hash t is a wrapper around F. It is the hash of a value of type t.
  5. Root t is a wrapper around F. It is the root of a Merkle tree with leaves of type t.
  6. Circuit is a set of commitments to the constraints of the circuit.

Symbolic Ledger types

  1. Address is of type Hash Circuit. The circuit describes the smart contract that locks funds at this address.

  2. TransactionEnvelope is a record type with the following fields:

    • txeAddress is of type Address. It is the address that initiated the transaction.
    • txeTransactionId is of type F.
    • txeValidityInterval is of type (POSIXTime, POSIXTime). It is the transaction's validity interval. The bounds are inclusive.

  3. BridgedInUTxO is a type describing a UTxO bridged in from Cardano.

  4. BridgedOutUTxO is a type describing a UTxO bridged out to Cardano.

  5. TransactionBatch is a record type with the following fields:

    • tbTransactions is of type [TransactionEnvelope]. It is a list of transaction envelopes included in the batch.
    • tbBridgedInUTxOs is of type [BridgedInUTxO].
    • tbBridgedOutUTxOs is of type [BridgedOutUTxO].
    • tbValidityInterval is of type (POSIXTime, POSIXTime). It is the batch's validity interval. The bounds are inclusive.
    • tbReference is of type Hash TransactionBatch. It is the hash of the previous batch.

  6. TransactionBatchCompressed defines the compact representation of the Symbolic Ledger state transition.

Validation rules

We now describe the Symbolic Ledger state transition rules. The validation logic is as follows:

  1. Starting from an empty batch, we apply transaction envelopes one by one, modifying the current batch object. An empty batch is a batch with an empty tbTransactions field and with other fields initialized from the data coming from the underlying blockchain.
  2. We set the batch validity value to Hash [].
  3. Every transaction application results in a modification of tbTransactions field. Bridged-in UTxOs and outputs produced in the batch transactions cannot be used immediately in the other transactions of the batch.
  4. For every transaction envelope, we do the following checks:
    1. The validity interval of the transaction envelope must be within the batch validity interval.
    2. We prove that the transaction validation function (see Symbolic Transactions) applied to the current batch validity value, the current batch object, and the transaction envelope returns a particular value. If its first output is 0, we consider the transaction envelope to be valid. Otherwise, we consider it to be invalid. We update currenty batch validity value with second output of this function.
  5. After the batch is constructed, we check that the current batch validity value is Hash [] (no value is created or burned).

  6. The finalized batch is compressed into TransactionBatchCompressed object.

    Note

    The TransactionBatchCompressed object is what is posted on the blockchain. In the on-chain smart contract, we verify a zero-knowledge proof that it was constructed as described above.