Plus tôt ce mois-ci nous avons rendu public le code source du langage blockchain Simplicity.
Simplicity est notre réponse aux problèmes que pose la programmation de smart contracts dans un environnement blockchain. Avant Simplicity, les langages de programmation blockchain devaient faire des compromis entre expressivité et fiabilité. Les développeurs pouvaient soit construire des_ smart contracts_ complexes mais peu fiables, ou des très basiques mais fiables. Avec Simplicity, les développeurs peuvent enfin concevoir des smart contracts sophistiqués et avoir confiance dans le résultat obtenu.
Simplicity a été conçu pour être compatible avec la plateforme Elements de Blockstream. Cela signifie que les développeurs qui construisent des sidechains ou des blockchains indépendantes avec Elements pourront bientôt profiter des possibilités proposées par Simplicity. En tant qu’implémentation d’Elements, le réseau Liquid prend en charge Simplicity, ce qui offrira des applications intéressantes pour les utilisateurs de Liquid, telles que le séquestre à confiance minimale, les coffres et d’autres smart contracts complexes.
La source publiée ce mois-ci comprend :
- Une sémantique dénotationnelle du coeur du langage Simplicity et de ses extensions spécifiée formellement dans Coq.
- Une sémantique opérationnelle du coeur du langage Simplicity spécifiée formellement dans Coq.
- Un interpréteur, un vérificateur de types, et une sérialisation du langage Simplicity écrite en Haskell.
- Des exemples d’expressions de Simplicity, y compris des opérations cryptographiques telles que SHA-256 et la vérification de signatures EC-Schnorr.
- Un rapport technique détaillant le langage Simplicity.
Pourquoi Simplicity ?
Les blockchains posent des défis uniques qui rendent les langages de programmation traditionnels peu adaptés.
- Tous les utilisateurs doivent s’accorder sur le résultat d’une opération dans n’importe quel environnement.
- Chaque participant du smart contract doit connaître en avance tous les résultats possibles pour toutes les données entrantes possibles d’un programme.
- Tous les utilisateurs doivent être en mesure d’empêcher une attaque par déni de service qui consommerait une part excessive de mémoire ou de temps de processeur.
- Chaque participant d’un smart contract _doit être en mesure d’estimer en avance les coûts de l’exécution de son programme pour tous les _inputs possibles.
Les langages déjà existants spécifiquement conçus pour les blockchains, tel que l’EVM d’Ethereum, n’ont toujours pas surmonté ces défis. Dernièrement, une mise à jour d’EVM a échoué en phase de test parce que les différentes implémentations ne s’accordaient pas sur le résultat d’une opération. Des fonds ont été volés ou irrémédiablement perdus à cause d’erreurs logiques dans les smart contracts et de programmes qui ont dépassé les limites des ressources disponibles.
D’un autre côté, le Script de Bitcoin se limite généralement à des combinaisons de vérification de signatures numériques, timelocks et hashlocks. Même si des protocoles impressionnants (comme le réseau Lightning) ont été construits sur ces primitives, le Script Bitcoin n’a pas l’expressivité requise pour des smart contracts plus complexes.
Simplicity a pour ambition de fournir l’expressivité et la flexibilité nécessaires pour toutes les opérations dont vous avez besoin, tout en permettant de vérifier la fiabilité, la sécurité et le coût de vos smart contracts.
Qu’est-ce que Simplicity ?
Simplicity est un langage de bas-niveau et un modèle machine pour des smart contracts basés sur une blockchain. Il est conçu pour avoir une sémantique simple qui se prête à l’analyse statique et aux raisonnements par des méthodes formelles. Simplicity est défini par son implémentation dans l’assistant de_ Coq proof._
Même si le coeur du langage lui-même est suffisamment simple pour tenir entier sur un T-shirt, sa simplicité ne se traduit pas dans le développement. Il y a plusieurs raisons à cela :
- Le développement sur blockchain implique un modèle radicalement différent de la programmation ordinaire. Le travail d’une blockchain est de vérifier le résultat des opérations plutôt que de les exécuter. C’est une distinction subtile, mais néanmoins extrêmement puissante parce qu’il est possible de vérifier le résultat de l’exécution de code arbitraire sans qu’il soit “Turing-complet”.
- Une fois déployé en production, un smart contract est immuable et ne laisse aucune marge de manoeuvre pour corriger les erreurs. Simplicity répond à ce problème en donnant le pouvoir à l’utilisateur de créer des preuves formelles de validité pour leur smart contracts.
- Simplicity est un langage de très bas-niveau pour une exécution directe, plus proche de l’assembleur que de Java ou Python. Nous pensons qu’à terme les utilisateurs écriront leur contrats dans un ou plusieurs langages de haut-niveau qui seront ensuite compilés en Simplicity.
Quoi de neuf ?
Depuis notre dernier post de blog sur Simplicity, nous avons travaillé dur pour passer de la recherche sur un langage expérimental à une spécification plus formelle.
Nous avons ré-implémenté dans le Coq proof assistant :
- Nous avons une sémantique dénotationnelle pour l’intégralité de Simplicity, y compris les extensions qui gèrent les données témoins, les assertions, et la délégation.
- Une spécification formelle pour une machine abstraite appelée “the Bit Machine”, basée sur des catégories libres, fournit la sémantique opérationnelle pour le coeur de Simplicity.
- Une implémentation en Haskell développée en tagless final style vous permet d’expérimenter en évaluant, exécutant et vérifiant les types des expressions écrites avec Simplicity.
- L’approche modulaire des extensions de Simplicity permet d’ignorer les effets des extensions quand vous ne les utilisez pas.
- Nous avons de nombreuses expressions écrites en Simplicity pour les primitives cryptographiques, y compris notre propre ré-implémentation de libsecp256k1 en Simplicity.
- Un rapport technique qui fournit une spécification mathématique informelle du langage et le manuel pour les développements de Coq et de Haskell.
Alors que le développement de Simplicity suit son cours, nous avons atteint le point où les développeurs peuvent explorer le langage par eux-mêmes. Il est donc temps de l’ouvrir et nous avons mis en place une mailing list.
Et ensuite ?
Plusieurs fronts nous attendent concernant le développement de Simplicity.
Pour notre part, nous prévoyons de :
- Compléter l’interpréteur C.
- Implémenter une librairie de jets pour diverses fonctions cryptographiques courantes.
- Utiliser Verifiable C pour prouver que notre interpréteur C et nos jets sont bons.
- Intégrer Simplicity dans la plateforme blockchain Elements.
Les autres chantiers comprennent :
- Le développement d’optimiseurs de code pour Simplicity.
- La création de nouvelles, ou l’adaptation des plateformes de _smart contract _de haut-niveau déjà existantes, telle que Ivy, pour générer du code Simplicity.
- La combinaison de la correction fonctionnelle des primitives cryptographiques de Simplicity avec les protocoles cryptographiques de correction formelle pour construire des smart contracts totalement vérifiables.
Nous espérons que vous vous joindrez à nous sur ce projet.