Archetype 1.0 Release!

We are very glad to announce the release of version 1.0 of the Archetype language! We want to thank everyone who provided us with early feedback and helped us improve the design of the language during the alpha phase. We also want to thank the great Tezos developer community for their technical support.

What is Archetype?

Archetype is a high-level Domain-Specific Language (DSL) to write smart contracts for the Tezos blockchain.

The decision to design a high-level DSL was driven by the fact that a smart contract has very specific features that we believe need to be taken into account at the development language level.

A smart contract is a highly critical, publically available short piece of code. Oftentimes, smart contracts control large amounts of value and therefore require high levels of security.

A bug in a smart contract may indeed annihilate the entire validity of a blockchain business process; it is public by design for everyone to know what the contract is about; it is not meant to be a large program as it is focused on the core business logic of data and crypto-money transactions.

As a consequence one of the key features we should expect from the code of a smart contract is its capacity to convey trust about what it does (or does not).

As a high-level specific language, Archetype enables the formulation of the business logic with concise and specific abstract concepts; it is thus easy to read and to figure out what it does.

Archetype also enables the formulation of what the contract is supposed to do (ie. its specification) with logical formula. The first virtue is to document the contract’s code with unambiguous formal statements, and the second virtue is to enable its formal verification (with why3 by transcription to whyml).

High-level features

Rationals, dates, durations

Rational, date, and duration values are available to formulate business logic.

For example, say the quantity of tez (Tezos tokens) transferred to a contract is converted to the expiration date until which the caller may use a service, by applying a conversion rate:

The formula line 14 illustrates the capacity to express contract’s logic with concise formula:

expiration := now + rate * t * 1h

The duration value is obtained by multiplying the transferred amount t (converted to integer line 13) by the rational value rate; it is converted to duration by multiplying it by 1h (one hour); it is then added to the date now to get a new date value.

Assets management

Data are organized as collections of assets. An asset is a record of values.

Say you want a smart contract to manage an ideas box so that:

  • anyone can add an idea
  • voters are granted with 5 voting tokens to put on the idea(s) they prefer
  • the box’s chairman finalizes the vote by selecting the top 3 ideas, with the constraint that a selected idea has collected at least 5 tokens.

The contract stores collections of 3 assets: ideas, voters, and selected ideas when finalized.

This automatically creates the corresponding (empty) asset collections. Asset collections come with a rich built-in API to modify, iterate, and aggregate assets.

The entry point below for the chairman to finalize the ideas box by selecting the top 3 ideas illustrates some of this API:

The entry point is made of several sections (called by, require, effect) which make the execution rules explicit. For example, it fails if the caller of the entry is not the chairman, if it is called before the expiration date, or if some ideas have already been selected.

The core voting logic holds in the iteration process line 63:

idea.select(the.nbvotes >= 5).sort(desc(nbvotes)).head(3)

Ideas are selected, sorted in descending nbvotes order, and trimmed with the top 3 ideas.

The vote entry may allow any registered voter to spend voting tokens on the ideas of choice during 2 days before the expiration date:

The date restriction rule line 38 is concise and explicit:

expiration - 2d < now <= expiration

Requirements’ ids, like r1, are used to generate messages; for example, calling the contract from a non registered address generates the following:

At last, entries to add ideas before the voting period, and for the chairman to register voters, are added to the contract:

Specification

Entry points may specify the effect they have on the contract storage.

For example, you may specify that the vote entry point may decrease the remaining field of the caller by the weight input parameter:

It is also possible to specify a property the contract’s storage must verify at any time; such a property is called an invariant.

For example, at any time, the total number of voting tokens must be equal to the sum of tokens received by ideas and the sum of remaining tokens:

Variables and assets may also be equipped with invariants. For example, the voter asset may be equipped with an invariant that states that the value of remaining is greater or equal to 0.

Once transcoded to whyml by Archetype, why3 transforms invariants and postconditions into proof obligations for solvers to verify.

A complete example of contract verification with why3 was exemplified in this article:

Verify a smart contract with Archetype

How it works

Archetype is not a compiler to Michelson, rather a transcoder to other languages.

In version 1.0, the execution language of choice is Ligo. Other languages like SCaml and SmartPy are coming soon. The language for formal verification is whyml, the language of the why3 framework.

The transcoding process consists of generating an intermediate representation of the contract, and then print it accordingly to the target language syntax.

This intermediate representation is transformed and specialized thanks to model transformations. An example of such transformation is the one that transforms entry points to pure functional effect-less functions, for languages like SCaml.

Archetype is open-source: feel free to contribute a new printer for the language of your choice.

Contract library

Archetype comes with a rich library of contract templates spanning several processes and domains:

  • escrow
  • finance
  • digital assets
  • IoT
  • governance
  • insurance

The ideas box presented above is one of the contracts in the governance section.

Resources

Please refer to the online documentation.

Follow the project on twitter.

10 Likes

Thanks for the post, any tutorial on how to deploy the contract? What about testing a contract written in Archetype?

Hi, thanks for your feedback. Archetype transcodes typically to Ligo. From there you may use Ligo’s deployment process. As a side note, the archetype VSCode extension generates Michelson straightforwardly if Ligo is installed. https://docs.archetype-lang.org/usage. Regarding testing, again you may use the Ligo interpreter, or the simulation feature of better call dev when deployed.

1 Like