L’année dernière, en octobre 2019, nous avions décrit l’écosystème Tezos (non exhaustivement) dans un premier article de blog, en faisant des zooms sur Michelson, Ligo, SmartPy, PyTezos. Pour cette seconde mouture, en mode “newsletter in french”, nous allons voir quelques points marquants de l’année 2020 : les nouveaux protocoles, les améliorations des langages, les standards de token, les preuves de smart contracts.
Cet article aborde plusieurs éléments de l'écosystème Tezos. Ce schéma permet de cartographier les sujets abordés. A gauche les outils de développement permettent de produire des smart contracts (scripts en Michelson), qui peuvent être déployés sur la blockchain. En haut, le réseau Tezos diffuse l’information à travers les nœuds afin de maintenir un registre commun immuable (blockchain); son protocole a été mis à jour. En bas, différents standards de token et projets remarquables ont été déployés. A droite, les outils d’analyse formelle permettent de faire des preuves de smart contracts (par exemple DEXter, une plateforme décentralisée d’échange de crypto-monnaie).
Vue simplifiée de l'écosystème Tezos
Injection effectuée ! Non, nous ne parlons pas du vaccin contre la COVID-19, mais bien du dernier protocole de Tezos : 007 Delphi.
Longue vie à la gouvernance on-chain ! Longue vie à Tezos !
Je rappelle que ce principe d’évolution par la modification du protocole (soumis à un vote) est un mécanisme appelé gouvernance on-chain qui permet d'éviter un découpage de communauté (que la communauté Tezos se sépare en 2 blockchains séparées pour des raisons techniques).
Petit rappel, voici une liste de ses prédécesseurs :
| Protocole | Date d’injection | Produit par |
| 004 Athens | 28 février 2019 | Nomadic Labs |
| 005 Babylone | 26 Juillet 2019 | Nomadic Labs |
| 006 Carthage | 14 Novembre 2019 | Nomadic Labs |
| 007 Delphi | 12 Novembre 2020 | Nomadic Labs, Metastate |
| 008 Edo | Pas encore injecté |
Protocoles injectés sur la blockchain Tezos
Le protocole Carthage améliore le langage Michelson en ajoutant de nouvelles instructions (sucre syntaxique) et la gestion d’annotation, en optimisant l'interpréteur et le typechecker.
Le changelog est disponible ici.
Le protocole Delphi intègre les améliorations suivantes :
Le changelog complet est disponible ici.
Le futur protocole Edo est en discussion et prévoit des améliorations telles que :
Le changelog complet est disponible ici.
Dans l’article Tezos Ecosystème - octobre 2019, nous avions décrit différents langages (transpiler) en cours de développement. Ces langages ont été améliorés et ont atteint un bon niveau de maturité.
A date il existe Ligo et SmartPy, Morley a été créé en 2020.
Nous avions vu en novembre 2019, que langage LIGO permettait de gérer quasiment toutes les instructions du Michelson, à l’exception de l’instruction CONTRACT (cas où un entry point précis est spécifié). Ceci a été remédié en LIGO avec la fonction get_entrypoint_opt. Pour rappel, cette fonction permet de connaitre la signature d’un entrypoint d’un smart contract (alors que get_contract_opt récupère tous les entry points d’un contrat).
Cette fonction get_entrypoint_opt a été ajoutée au transpiler LIGO et permet de travailler avec des signatures partielles de contrat. Maintenant, il suffit de connaître uniquement la signature d’un entrypoint pour pouvoir appeler cet entrypoint. Et donc elle permet donc de faire communiquer (bi-directionnellement) des smart contracts avec des smart contracts déjà déployés sur la blockchain Tezos.
La génération de code Michelson a également été optimisée, produisant un code moins long et diminuant ainsi le coût en gaz lors du déploiement ou de l'exécution d’un smart contract.
Comme les autres transpilers précédemment mentionnés (LIGO, SmartPy, …), le but de Morley est de faciliter l’écriture de smart contract Michelson. La particularité de Morley est d’être plus proche (syntaxiquement parlant) du Michelson que les autres transpilers ce qui offre une approche plus fine vis-à-vis du code Michelson et potentiellement un smart contract parfaitement optimisé (comme s’il avait été codé en Michelson directement).
Morley est constitué des 3 composants suivants :
La plateforme décentralisée d’échange de crypto-monnaie (ou “Decentralised exchange”) DEXter implémente des smart contracts écrits en Morley. Le code des smart contracts est disponible ici.
Voici un petit exemple de code provenant du projet DEXter (GitLab du projet ici) pour illustrer !
E_xemple de code Morley_
On peut remarquer que le Morley est très proche du Michelson avec l’utilisation d’instructions (duuupX et dip (dip ())).
On remarque également la possibilité d’écrire plusieurs instructions par ligne, et de mettre des commentaires, et autre sucre syntaxique comme le if.
La documentation détaillée de Morley est disponible ici.
La tokenisation est un sujet bien connu dans le monde de la Blockchain. Jusque-là les propositions de standard viennent de la blockchain Ethereum avec les 2 standards les plus connus (ERC20 et ERC721). Dans l'écosystème Tezos, ce standard est connu sous le nom de FA1.2 (Financial Application 1.2) et est très utilisé notamment par les wallets (thanos), le protocol Nyx, ou les exchanges décentralisés Dexter (source) et Quipuswap (source).
Des initiatives ont été lancées pour améliorer ce standard de tokenisation avec deux propositions TZIP-12 et TZIP-16 (pour rappel, TZIP signifie Tezos Improvement Proposal).
L'implémentation de la proposition TZIP-12 ou communément appelé FA2 a été faite principalement par :
Elle apporte des améliorations :
L'implémentation de la proposition TZIP-16 qui prévoit la gestion de métadonnées associées aux smart contracts est en cours de développement (ici).
Le but de TZIP-16 est de permettre une meilleure gestion des métadonnées; c’est-à-dire l’ensemble des informations disponibles sur le contrat qui sont habituellement utilisées off-chain (en dehors de la blockchain), comme par exemple l’auteur d’un smart contract, les copyrights, la description d’un smart contract, ou des vues dites “off-chain”.
Les vues “off-chain” sont des requêtes (API REST) que n’importe qui peut exécuter off-chain pour obtenir des informations sur le storage d’un contrat.
Cette section fait le point sur les smart contracts prouvés (non exhaustif) et les axes d’amélioration de la preuve sur les smart contracts Tezos.
Dans le premier article sur Tezos et la vérification formelle, nous avons introduit les assistants de preuve et donné un exemple d’assistant de preuve Coq. Plusieurs smart contracts ont déjà été prouvés grâce à Coq et Mi-cho-coq (spécification formelle en Coq du langage Michelson).
Voici quelques liens vers des preuves de smart contract fournies par Nomadic Labs (ici) en utilisant Coq et Mi-cho-coq:
Voici un tableau qui donne une idée du coût engendré par la réalisation de la preuve.
| Contrat | Taille du Smart contract (instructions) | Taille de la preuve (lignes) | Durée pour écrire la preuve |
| Manager | 24 | 175 | 1 personne-jour |
| Multi-signature | 92 | 620 | 1 personne-semaine |
| Spend Limit contract | 195 | 1132 | 3 personne-semaines |
| Dexter | 2324 | 2983 | 4 personne-semaines |
Coût de la réalisation de la preuve
On remarque pour Dexter, que la preuve devient très longue et sachant que la preuve est beaucoup plus complexe à écrire que le smart contract, la tâche d’écrire une preuve s’avère non négligeable ! Ce niveau de confiance dans le smart contract est conseillé pour des systèmes critiques, mais pas forcément pour tous les smart contracts.
Remarque: Une preuve de smart contract ne remplace pas un audit de sécurité (qui lui rassure de façon globale sur l’ensemble de l’utilisation d’un smart contract) et peut également inclure un audit de la preuve (des post-conditions).
Un autre assistant de preuve Archetype s’est fait remarquer cette année 2020 en produisant la preuve du standard FA1.2. Voici un exemple de smart contract prouvé par TQ Tezos à l’aide de l’assistant de preuve Archetype :
https://assets.tqtezos.com/docs/token-contracts/fa12/4-fa12-archetype/
Des initiatives lancées par Nomadic Labs sont en cours pour améliorer Mi-cho-coq et permettre ainsi la preuve sur une plus grande variété de smart contracts. Voici quelques axes d’amélioration prévus pour 2021/2022 :
preuve sur des interactions entre smart contracts :
Gas model :
Preuve sur les propriétés temporelles (“time properties”)
Le principe de gouvernance “on-chain” implémenté par Tezos montre qu’il est possible d’améliorer le protocole (amélioration du langage , optimisation, sucre syntaxique) sans provoquer de dilution de la communauté. Rien que pour ça, je pense que Tezos mérite son titre de blockchain de 3ème génération.
Le langage LIGO, maintenant complet permet de construire des systèmes plus complexes graĉe à la communication inter-contrat (facilitée avec fonction get_entrypoint_opt). Reste à voir si les coûts d’interaction entre contrats ne deviennent pas trop élevés en gaz !
Le Morley commence à faire sa place dans l’écosystème Tezos, avec l'implémentation d’un DEX (decentralised exchange).
De nouvelles améliorations concernant les standards de token (fongible, non-fongible, multi-asset) et notamment avec une prochaine version (TZIP-16) qui proposera une meilleure gestion des métadonnées.
De nouveaux smart contracts ont été prouvés, par exemple sur DEXter (une plateforme d’échange décentralisée). C’est une nouvelle milestone qui a été franchie dans le monde de la preuve de smart contract. Cependant l’impact de la preuve ne se fait pas encore sentir, potentiellement à cause du coût pour produire une preuve (travail complexe fait par des experts).
Des améliorations de Mi-cho-coq sont prévues pour permettre la preuve sur l’interaction entre plusieurs contrats.