How to verify an existing contract with Archetype?
Two weeks ago we released Archetype 1.0. We’re thankful for the great feedback from the developer community.
A frequent point of feedback we‘ve been receiving from developers is the need to rewrite a smart contract in Archetype to be able to verify it with why3.
Transcoding to Archetype requires to map the source code to higher-level non-Michelson concepts such as durations, rationals, collections of assets with a rich API (select, sum, …), partitions of assets, etc.
These concepts have been introduced in Archetype to ease the formal verification process. Indeed the higher the level of expression of the business logic, the easier it is to verify a smart contract.
For example, in the ideas box contract in the Archetype contracts’ library, the selection of the top 3 ideas with a number of votes greater or equal to 5, is done with the following code:
idea.select(the.nbvotes >= 5).sort(desc(nbvotes)).head(3)
The following postconditions of the select operator are then automatically generated by Archetype:
forall k, mem k result → forall idk, idea.get(k) = some idk → idk.nbvotes >= 5
forall k, mem k result → idea.get(k) = none → false
Besides the fact that you need to be quite familiar with the Archetype API, the risk of transcoding manually to Archetype is that you may change the semantics of the program; the result is that you may believe the original contract has a property it does not have …
To address the need for contract verification, we are developing a feature to safely transcode an existing contract to Archetype.
The roadmap to this new transcoding feature, that is the roadmap to Archetype V2.0, is presented below:
The first milestone (M1) is to complete the Archetype language with all the concepts available in Michelson and higher-level languages like LIGO or SmartPy, mainly:
- nat type
- set, map containers
- record structure
The second milestone (M2) is the parsing and transcoding of existing contracts written in LIGO and SmartPy. At this step, the transcoding process maps source concepts (type, container, builtins, etc.) to their Archetype counterparts.
The third and last milestone (M3) consists of a set of program transforms to express the program logic with Archetype-specific concepts. Examples of such transforms are:
- transform containers (map, set, list) to collections of asset
- merge assets
- inject archetype asset API
- …
These transforms will be applied semi-automatically and will guarantee the semantic equivalence of the resulting program with the source.
In terms of next steps, M1 is in the pipe, and the corresponding version 1.1 is to be announced very soon. M2 should be available by end of September with support for LIGO and SmartPy (in that order).
Note that with the release of M2, it will already be possible to verify an existing contract (written in LIGO or SmartPy) with why3.
M3 will enable the use of high-level builtin asset API postconditions, which makes verification easier.
Resources
Please refer to the online documentation .
Follow the project on twitter.
