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.

Big picture

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

Protocole Tezos

007 - permis d'injecter

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 :

Protocoles injectés sur la blockchain Tezos

Évolutions du protocole

Rappel de ce qu’avait apporté Carthage

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.

Ce qu’apporte Delphi

Le protocole Delphi intègre les améliorations suivantes :

• diminution des coûts de stockage
• amélioration/sécurisation de l'interpréteur Michelson (en limitant le nombre d’appels récursifs)
• amélioration du langage Michelson (gestion des annotations, optimisation)
• augmentation (x3.5) du nombre de transactions (transfert de XTZ) par bloc
• augmentation (x4) du nombre de transactions (transfert de token FA2) par bloc
• diminution du coût en gaz de l'exécution des instructions des smart contracts

Le changelog complet est disponible ici.

Ce que prévoit Edo

Le futur protocole Edo est en discussion et prévoit des améliorations telles que :

• Sapling : technique permettant de préserver la confidentialité lors de paiement sur un ledger publique. (plus de détails ici)
• Tickets : un Ticket permet d’authentifier une donnée par rapport à une adresse Tezos, permettant ainsi de construire un système permissionné (article de vulgarisation ici)

Le changelog complet est disponible ici.

Les langages / transpilers

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.

Amélioration LIGO

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.

Morley

Yet another transpiler

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 :

1. un exécutable qui permet de simuler les interactions avec un smart contract Michelson
2. une librairie contenant les spécifications du langage Michelson, les API de Tezos et autres outils d'interprétation de code Michelson :
   • outils de cryptographie
   • typechecker (pour valider un script Michelson)
   • interpréteur (pour exécuter un script Michelson)
   • parser (pour transformer un smart contract Michelson en un script Haskell ADT)
   • interface d'exécution
3. le langage Morley (spécifications) qui est une surcouche du langage Michelson un peu plus “user-friendly” :
   • le parser accepte une syntaxe plus souple
   • ajout de sucre syntaxique, et de fonctions “helpers”

Projet implémenté en Morley

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.

Token standard

FA1.2

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).

FA2

L'implémentation de la proposition TZIP-12 ou communément appelé FA2 a été faite principalement par :

• Eugène Mishura de TqTezos (pour la version CameLigo)
• Matej Sima de StoveLabs (pour la version ReasonLigo)

Elle apporte des améliorations :

• standardise la gestion des métadonnées des tokens (définition, nom, symbole, unité, fongible) et permet de gérer plusieurs tokens (“multi-asset”)
• standardise l’interaction de demande de balance ou de métadonnées

Dans le futur (TZIP-16)

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.

Preuve sur des contrats Tezos

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.

Preuves de smart contracts

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:

• Proof of Multi-signature contract (ici)
• Proof of Voting contract (ici)
• Proof of Spend Limit contract (for cortez wallet) (ici)
• Proof of Dexter (ici)

Voici un tableau qui donne une idée du coût engendré par la réalisation de la preuve.

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/

Mi-cho-coq dans le futur

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 :

  • Il n’est toujours pas possible de faire de preuve sur des smarts contracts qui utilisent l’instruction CONTRACT (c’est-à-dire l’interaction de plusieurs smart contracts)
  • Des initiatives sont planifiées pour permettre la preuve sur des smarts contracts qui interagissent graĉe à ConCert (début projet IMDEA)

• Gas model :

  • génération automatique du “gas model”
  • amélioration de la documentation liée au gas model

• Preuve sur les propriétés temporelles (“time properties”)

Conclusion

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.