Meanwhile at Cryptium Labs #1 Part IV

Awa Sun Yin
Jun 20 · 4 min read

If you haven’t read them yet, here are links to Part I, Part II, and Part III. In Part IV, another feature we are working on is described: simplifying Tezos smart contracts, in order to facilitate formal verification and increase maintainability of accounts.

This article starts with a recap of Michelson and smart contracts on Tezos. Secondly, the background outlines some of the current limitations of Tezos smart contracts. This is followed by a description of motivations or goals behind these changes. Finally, a description of the implementation.

Meanwhile at Cryptium Labs #1 Part IV: Simplifying Tezos Smart Contracts

Recap of Michelson & Tezos Smart Contracts

Michelson is the programming language in which smart contracts on Tezos are written. Unlike well-known smart contract languages, it is characterised for being stack-based. A Tezos smart contract is a collection of Michelson instructions. For illustration, using an Ethereum-related example, Michelson is as low-level as EVM bytecode. In every smart contract, an instruction is represented by uppercase identifiers, for instance EQ, which checks that the top of the stack is equal to 0:

:: int : 'S   ->   bool : 'S> EQ / 0 : S  =>  True : S> EQ / v : S  =>  False : Siff v <> 0

Generally, due to practicality, decentralised application or smart contract developers tend to program in higher-level languages that later compile down to the lower level language that is executed by the state machine.

Examples in Michelson

*And formally verified by Nomadic Labs, you can find the proofs on GitLab.

Examples in Liquidity

Background

Smart Contracts that Are Not So Smart

So far, all delegations on Tezos have been made using implicit accounts in combination with originated accounts, causing the deployment of a substantial amount of smart contracts that are script-less, containing no Michelson code or instructions, and only carrying hard coded values within the underlying storage.

In addition to the transactions that wallets or other clients generate, there are currently Michelson instructions that were introduced by inertia, taking the existing process for making delegations into consideration. The Michelson instructions in question are CREATE_ACCOUNT and CREATE_CONTRACT.

Unnecessary Logic in Smart Contracts

Another limitation derives from the fact that whenever a smart contract is deployed, it will carry the logic and features that enable delegations, albeit the purpose of this particular smart contract is unrelated. This unnecessary logic increases the complexity of the program, deeming it harder to formally verify.

Motivations

As this multi-step process to make a delegation will no longer be necessary after implicit accounts are delegatable, meaning that users will be able to delegate directly through their TZ1 accounts (see: Part III on simplifying the delegation process), a desirable outcome is to prevent the future creation of script-less smart contracts, as well as enabling the ability to create smart contracts that do not carry unnecessary logic.

The purpose behind the changes described below is to simplify formal verification of smart contracts, by reducing the complexity that is derived from the default delegation-related logic that every smart contract carries, as well as easing the maintainability of code, by simplifying the accounts system.

Simplifying Smart Contracts

To prevent the future creation of script-less accounts*:

  1. Deprecating the CREATE_ACCOUNT instruction, to avoid the future creation of script-less smart contracts.
  2. Modifying theCREATE_CONTRACT instruction by removing manager, delegatable, and spendable parameters. To prevent the future smart contracts carrying unnecessary logic.

*Note that this prevents future deployments of script-less smart contracts, but already deployed ones will not be affected.

In combination of the above changes to Michelson instructions, there will be CLI changes that affect the transactions that wallet developers are sending to interact with accounts, so wallets will no longer be able to create script-less accounts. Instead, they will be able to enable delegations directly through the implicit accounts.

However, it will no longer be necessary after implicit accounts are delegatable and users will be able to delegate directly through their TZ1 accounts (see: Part III on simplifying the delegation process).

The implementation of these changes is open-source and can be found here:

Final Remarks

In Part IV, we describe another set of features we are working on, which aims to simplify Tezos smart contracts with the purpose of making their formal verification easier, as well as easing the maintainability of code derived from a simpler accounts system.

This feature, just like all other features, will be proposed in the upcoming Proposal period. Nevertheless, it must be voted by the community to be adopted.

Follow us on Medium and Twitter to Stay Tuned! 🐫

Cryptium Labs Tezos

Cryptium Labs offers secure and highly available digital signatures for Proof-of-Stake networks, such as Tezos, Cøsmos, and Polkadot. This blog is dedicated to anyone in the blockchain ecosystem and aims to provide educational content for all audiences on topics such as security.

Awa Sun Yin

Written by

Founder @ Cryptium Labs

Cryptium Labs Tezos

Cryptium Labs offers secure and highly available digital signatures for Proof-of-Stake networks, such as Tezos, Cøsmos, and Polkadot. This blog is dedicated to anyone in the blockchain ecosystem and aims to provide educational content for all audiences on topics such as security.