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).
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.
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 (
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.
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:
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:
How it works
Archetype is not a compiler to Michelson, rather a transcoder to other languages.
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.
Archetype comes with a rich library of contract templates spanning several processes and domains:
- digital assets
The ideas box presented above is one of the contracts in the governance section.
Please refer to the online documentation.
Follow the project on twitter.