A constraint-based UTXO model (2/4)
Ledger and transaction models
There are well known UTXO transaction models and implementations, such as Bitcoin, Cardano’s Extended UTXO (EUTXO), the Stardust by IOTA Foundation and others. Not going into detail, we just note here, that fundamentally all these models are constraint-based transaction ledgers, as per nature of UTXO. In this sense they are all equivalent, i.e. we cannot say that one model can do something what the other fundamentally can’t, we can only discuss how good or bad UX/DX or implementation is.
In contrast, the transaction models of Ethereum, IOTA Smart Contracts (ISC) and many others (most, actually) we call execution-based.
Now we have to explain, what the constraint-based means. We will try to do it by summarizing differences between constraint-based and execution-based in the table below for the use Alice.
(in the table we intentionally ignore double-spend-induced non-determinism, because it essentially is outside the ledger as such. It is irrelevant to explaining what the “constraint-based” means. But see also the the comment below)
(here is the link to the halting problem)
So, there are two different modes of interaction with the ledger:
- with constraint-based ledger: Alice submits the transaction T to the ledger, the ledger checks the validity of T and either (a) appends it to the ledger, or (b) rejects it without any side effects:
- with execution-based ledger: Alice submits a request (the calldata), then the ledger executes the request by applying it to the (non-deterministic) state. The transaction is never rejected. The failing of the request, for example due to not enough funds, is also a settlement of that fact on the ledger:
Note. By submitting a transaction or request, Alice always faces certain non-determinism from the network, which is not strictly ledger-related. In the execution-based case (think Ethereum, ISC), the source of not-determinism is the asynchronous ledger state, while in UTXO the non-determinism may come from ledger conflicts, aka double spends. Someone else can try to spend the same input (which is why the ledger better set constraints to prevent that, but that is another story). The job of the consensus is to resolve the conflict, so it is unpredictable, in general. In UTXO ledgers, the consensus often acts as a sequencer (see Bitcoin, Cardano, Fuel), however that is an inefficient form of sequencing in case of high TPS to the same shared state (think same asset). For this reason, a performant smart contract system based on UTXO-bound states will need a sequencer. The discussion on this topic is outside the scope of this write-up.
We can see the two above are based on a different set of assumptions. Fundamentally, the strategic choice is between UTXO and non-UTXO, with different tradeoffs, mostly different ledger capacities/throughput and shared global state. The UTXO is constraint-based by its very nature. Its nature does not like unbounded global states and non-determinism, traits of the real smart contracts. With EasyUTXO we focus on constraint-based choice with open architecture, while leaving the whole smart contract drama for the possible future.
EasyUTXO uses a simple functional language EasyFL as a constraint language. The finite constraints of EasyFL provide programmability for use cases which are naturally parallelizable on the UTXO ledger. The use-cases which require unbounded state and global assumptions, like all kind of on-ledger searchable databases, such as registries of (domain) names, black/white lists, global accounts, one will need more powerful computation environments with traversal (loops) and unbounded data structures. The EasyFL does not provide it by intention.
EasyUTXO is a PoC. It implements (in EasyFL) many ledger constraints, equivalent to the Stardust output types and feature blocks: chain constraint (Alias/NFT/identity equivalent), time locks, expiry, NFT royalties, immutability etc. With PoC we had to stop at some point, but possibilities are limitless. New output types can be added later, dynamically, in order to implement a broad class of use cases.
Transaction. Outputs
The UTXO ledger state consists of UTXOs (Unspent TransaXtion Outputs) or simply outputs. Each UTXO is uniquely identified on the ledger globally and forever by its output ID, which is a concatenation of the hash of the transaction it was produced by, and the index of the output:
outputID = transactionHash || indexOfTheOutputInTransaction.
Each UTXO represents an atomic asset (the UTXO asset) on the ledger. It usually contains the number of fungible tokens (the amount), it can be an NFT or other asset: it all is a matter of conventions. The UTXO asset (the output) can be spent (or consumed) by a transaction. After consumed, the output disappears from the ledger state and some other UTXOs, the ones produced by the transaction, will appear on the ledger state as unspent.
Thus UTXO transaction represents a ledger state transition by consuming UTXOs (also known as inputs) and producing new UTXOs.
The whole point of the ledger is that it only allows consistent (valid) states. This is equivalent to saying that only valid transactions can be added to the ledger. The EasyUTXO makes sure the transaction is valid by enforcing all relevant constraints of the transaction are satisfied.
In EasyUTXO transaction as a data structure is a tree with byte arrays as leaves (see picture). Each node of the tree can have up to 256 children. Each node can be interpreted as a byte array, as a recursive concatenation of its children. Outputs in the transaction are nodes of the tree. Each output can be treated as a byte array, which can be parsed into the array of constraints (see below).
The full transaction in EasyUTXO consists of
- consumed outputs
- produced outputs
- other transaction data: unlock parameters, signatures, transaction timestamp, input commitment and local library
The part of the full transaction, the transferable transaction, is the part which is transferred over the wire between nodes. It does not contain consumed outputs because they already supposed to be on the ledger as immutable UTXOs.
Each data element in the transaction has a location in the tree called path, a sequence of byte values which leads to it in the tree.
- Path with prefix (1,0) leads to consumed outputs branch
- Path with prefix (0,2) leads to produced outputs branch
- Path with prefix (0,0) leads to unlock parameters branch
- Path (0) represents the whole transferable transaction
And so on. For example the path (0,2,7,1) leads to the 7th produced output and 1 is the index of the constraint in the output.
The path of a data element is the way how the constraint references and retrieves data element in the process of evaluation.
Constraints
The constraint is a boolean function (aka predicate) P(T) of the transaction T, which, when evaluated, renders true or false. In EasyUTXO it is represented by an EasyFL expression.
In the transaction, the output is created as produced output. After transactions is settled on the ledger, the same output will later appear as consumed output in some other transaction.
Each output is an array of constraints: O = (P1, P2, … Pn). Each Pi is a runnable bytecode of the EasyFL expression. The output is a concatenation of constraints.
All constraints (bytecodes of expressions) in the transaction are evaluated. If any of it is not satisfied, i.e. renders false, the whole transaction is deemed invalid.
Some constraints are mandatory. For example, we require every UTXO must be locked. Locking of the output means any output on the ledger can only be consumed by providing a signature of some sort (plus by satisfying other constraints). This way we prevent possibility to consume the same output by two different entities.
The special embedded function with name @ and no arguments always returns the path from the transaction root to the constraint currently being evaluated.
Any data element of the transaction tree (byte array, leaf or node) can be retrieved by the constraint formula with the embedded function @Path(<p>) , where <p> is the path of the element in the transaction tree. The expression @Path(@) always returns the bytecode of the current constraint itself. For convenience, it has a separate definition in the standard library as self . Its definition: func self: @Path(@)
Any data element of the transaction tree can be retrieved from the EasyFL expression. It can be an individual constraint, an output, all outputs concatenated or the whole transaction in its serialized byte form.
For example, (0) is the path to the transferable part of the transaction, so the expression @Path(0) will evaluate to the serialized form of transferable transaction bytes (without consumed outputs). The expression blake2b(@Path(0)) will return the transaction ID (hash of transferable transaction bytes). Similarly, blake2b(@Path(0x0100)) will return hash of all consumed outputs, i.e. the input commitment.
The output in EasyUTXO only contains executable code, the bytecodes of constraints. This way, the outputs are self-describing. Executing the outputs enforces validity constraints. Outputs do not contain a random data, interpreted only by the outside code. It must be a valid bytecode of the constraint.
Specification of the constraint-based ledger
Usually specification of the ledger, such as Stardust are semi-formal. Implementations in different environments may differ in minor detail. For formal verification of desired properties of such a specification, first we must write a formal specification in some formal language, so essentially create yet another implementation.
The constraint-based ledger offers more robust approach. Under very simple assumptions (axioms), the constraint specification and its implementation is essentially the same thing. It also is completely platform- and implementation-independent.
The EasyFL code can be used as is as input to the formal (automatic) prover to prove/validate desired characteristics of the ledger state. For example, such a validator could automatically answer questions such as “is it possible to unlock the output?” or “is it possible to create 2 chains with the same identity?”. That can be a life saver, for example when you want to be sure the innocent constraint in your output won’t lock your funds forever.
