A constraint-based UTXO model (3/4)

Transaction validation. EasyFL

Previous

Global constraints. Validation loop

Transaction is valid if it represents a valid ledger state transition, i.e. when added to the ledger, it preserves the consistency of the ledger.

By global constraint we call a validity condition which cannot be enforced by the local constraints on outputs. They are enforced from the outside of the ledger itself. In this sense, normally in UTXO ledgers all transaction constraints are global, because they are enforced by the external code contained in nodes such as Stardust.

Meanwhile, there are just few such global assumptions in the EasyUTXO, which are enforced not by the code committed in the transaction:

1. all local output constraints must be satisfied: the validation loop;
2. each consumed and produced output must contain at least the following 3 mandatory constraints: amount, timestamp and one of several known lock constraints (e.g. addressED25519, chainLock and few others). (In EasyUTXO we want each output belong to an account, ultimately controllable by signature, for reasons outside the scope of the ledger)
3. total value constrained by the amount constraints in consumed outputs must be equal to the total amount of the produced outputs (or adjusted to the on-transaction inflation rules)
4. the hash of all consumed outputs must be equal to the input commitment provided in the transaction (to prevent faked output attack).

So, the validation of the transaction is just one simple procedure to check global constraints. It is essentially a loop through all outputs which evaluates all their constraints. If all render true, transaction is valid. Otherwise it is invalid.

The ledger is the definition of its constraints.

Comparing to Stardust

The Stardust ledger works similarly to EasyUTXO (in the end, the both are constraint-based), however outputs there contain plain data interpreted by an outside code, the iota.go library. It checks syntactical validity of the transaction and validity of token balances and signatures. The output constraints in Stardust are implemented as output types and feature blocks. Each output type and each type of feature block, when added to the transaction, brings a specific set of constraints to it.

For example, Alias output enforces chain constraint and constraints specific to the Alias, such as chain controllers, the chain/NFT originator or immutable data by analyzing transaction and making sure the specific input and output makes a chain. The sender and expiry blocks are other examples of hardcoded constraints.

Stardust ledger always checks global constraints such as balanced left and right side of token amounts, unlock blocks and signatures.

All those conditions, hardcoded in the iota.go library, must be satisfied by the transaction. In contrast, in the EasyUTXO ledger the hardcoded part is just one simple loop, the rest is part of the transaction or is committed to it.

Another difference is that constraints in EasyUTXO are at byte level (see EasyFL below), i.e. bypassing any high level serialization logic. That makes them platform independent without the use of 3rd party conventions as Protobuf.

EasyFL

EasyFL is a (very) simple functional language, you can see it in the EasyFL repository, which contains the compiler, runtime engine, standard library of basic functions and many tests (never enough).

Being a formula language, it is much more user-friendly and easier verifiable than, for example Bitcoin Script or Algorand’s TEAL, which play the same role, and much simpler than Cardano’s Plutus Core, a dialect of Haskell. It also has much smaller executable bytecode than EVM, Plutus, WebAssembly, Move and the likes which assume much broader computation model: being universal has costs. Instruction overhead for EasyFL normally is few or few dozens bytes.

In EasyFL’s (almost) LISP-like syntax we write formulas or expressions. For example, when evaluated, the following expression with parameters $0and $1

if(lessThen($1,$0),sub8($0,$1),0)

renders $0-$1 if $1<$0, otherwise 0 in byte arithmetic. If argument data does not fit the byte arithmetic, the evaluation of the formula panics. The panic exception invalidates the whole transaction.

The semantics of the expression is a function call: f(P1,.. Pn), where Pi is an expression too. It hasn’t any side effects, because all underlying data is immutable.

To compose expressions, we use functions from the extendable runtime library. For example concat, slice, and, if, sub8 are examples of embedded functions from the global library. Most of them have obvious and trivial semantics, for example concat concatenates its arguments. The global library is hardcoded, i.e. shared by all nodes in the system. It can also be extended, both globally or in the transaction inline, with the user-defined local libraries, supplied to the transaction’s context.

The code of constraints is contained in the outputs in the form of highly compressed canonic bytecode. The bytecode is so simple that it can be parsed and analyzed by the EasyFL function itself (the standard library provides basic functions for that). For example, the bytecode of the constraint expression amount(u64/1337) may be parsed by the NFTRoyalties constraint to check if the uint64 value (1337) is enough tokens of royalties sent to the NFT originator.

The EasyFL uses only one data type: byte array. It is taken as an arguments and it is returned as a value. Wherever relevant, the 0-length byte array is interpreted as false, any other return value is interpreted as true. For example and(concat, 0x11) is always false because concat without parameters always returns empty array.

We can extend library by defining new functions as expressions. Recursive definitions are not allowed, hence the assumed computation model of the language isn’t Turing-equivalent.

Below is the definition the mandatory amount constraint:

// $0 - amount uint64 big-endian
func amount: and(
    equal(selfBlockIndex,0), // amount must be at block 0
    or(
        selfIsConsumedOutput,   // always satisfied in the consumed branch
        and(
            selfIsProducedOutput,  // checked in the produced branch
            equal(len8($0),8),     // length must be 8 bytes
            // must satisfy minimum storage deposit requirements
            storageDepositEnough($0)  
        )
    )
)

The constraint function amount takes one argument. The constraint must be located under index 0 in the output. Constraint amount(u64/1337) will invalidate the transaction, if the amount 1337 will be less than the required storage deposit. It will also invalidate the transaction if the argument will not be 8-byte long value. The bytecode of the compiled constraint expression amount(u64/1337) is0x457d880000000000000539, where 0x457d is the call prefix of the amount function, contained in the global library.

This way EasyFL constraints are on the data at the binary level, i.e. bypassing any serialization to/from high level language (HLL) data structures, used the external libraries written in HLL (the latter are still useful for transaction building and similar use cases). This makes EasyFL constraints completely platform independent, i.e. they will work same way in nodes written in Go, Rust, Python and so on without changes.

Next: Part 4. Unlocking the inputs. Examples