Meanwhile at Cryptium Labs #1 Part IV

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.

• The set of features described in this article are closely related to the ones described on Part III: simplifying the delegation process. Thus, I strongly recommend reading Part III before continuing.

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 : S
iff 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.

• For example, Ethereum smart contracts are normally written in Solidity, which is compiled into EVM bytecode. Similarly, a developer could write Tezos smart contracts in Liquidity or other supported higher level languages, which is later compiled to Michelson.

Examples in Michelson

• The Multisig written by
  Arthur Breitman
  *

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

Examples in Liquidity

• The Publisher contract written by
  Marty Stumpf
  and other smart contracts written in Liquidity in our GitHub repository.

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.

• For example, a script-less smart contract is created and deployed whenever a wallet sends a transaction to create KT1 account from an implicit account. In fact, most delegations (corresponding KT1 accounts) are script-less smart contracts.

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:

WIP: Origination deprecations (!3) · Merge Requests · Cryptium Labs / tezos

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! 🐫