Contrairement à la plupart des langages de programmation, les expressions Simplicity sont construites à partir d'une série de combinateurs, qui construisent des expressions à partir d'expressions plus petites. Ces expressions représentent des fonctions prenant une entrée et la faisant correspondre à une sortie.

Voici le programme Simplicity le plus simple :

main := iden

Ce programme prend une entrée vide et produit une sortie vide. Faisons quelque chose de plus intéressant, en prenant un bit et en l'inversant :

   bit0 := injl unit : 1 * 1 -> 2
   bit1 := injr unit : 1 * 1 -> 2

   padR := pair iden unit     : 2 -> 2 * 1 
   bitflip := case bit1 bit0  : 2 * 1 -> 2
   main := comp padR bitflip  : 2 -> 2

Ici, l'expression finale de Simplicity est la fonction main. En lisant de bas en haut, nous pouvons voir qu'il s'agit de la composition de plusieurs fonctions plus petites, qui finissent par se combiner en combinateurs unitaires. Les combinateurs unitaires produisent une sortie vide. Avec iden, qui prend une entrée arbitraire et la renvoie inchangée, et witness, qui produit une valeur fournie en externe, les combinateurs unitaires forment la base de chaque expression Simplicity.

Dans cet exemple de code, nous avons fourni les types de données pour aider à indiquer quelles données circulent entre chaque partie de l'expression. Ici, "1" représente le type d'unité, c'est-à-dire ce que nous appelons une "sortie vide". "2" représente un bit, qui peut prendre la valeur 0 ou 1.

Ne vous inquiétez pas si vous n'avez pas suivi cet exemple en détail. Il n'est là que pour montrer visuellement à quoi ressemble un code Simplicity. Plus loin dans cet article, nous analyserons plus en détail un programme plus intéressant.

Un langage de spécification

En réalité, tous les langages de programmation permettent de combiner des calculs pour en construire de plus complexes. Bitcoin Script (comme Forth ou PostScript) le fait au moyen de sa pile, dans laquelle chaque calcul utilise une liste d'objets de données un à la suite de l’autre. L'EVM d'Ethereum utilise une architecture d'appel de fonction où le code peut appeler d'autres blocs de code (éventuellement dans d'autres contrats), qui prennent des données en entrée et renvoient des données en sortie. C'est également le modèle utilisé par la quasi-totalité des langages de programmation aujourd'hui.

Les langages de programmation utilisent l'effet de bord pour interagir avec le monde extérieur, comme la transaction en cours de dépense. Dans l'EVM, les contrats ont également accès à des magasins de données clé-valeur, qui leur permettent de conserver l'état sans le transmettre explicitement.

Dans Bitcoin Script et EVM, l'inversion de bit peut être réalisée avec un seul opcode (bien que la version Bitcoin puisse prendre de nombreuses entrées différentes, dont la plupart ne ressemblent pas à des bits, tandis que la version EVM agit de manière bitwise, toujours sur 256 bits à la fois). On peut raisonnablement se demander pourquoi le modèle de Simplicity conduit à une telle verbosité pour des choses aussi simples.

Notre objectif avec Simplicity est de spécifier formellement la sémantique des programmes, à la fois en termes de fonctions qu'ils représentent et de ressources informatiques impliquées dans leur évaluation. Il serait possible, en principe, de spécifier formellement un langage qui fonctionne comme Bitcoin Script ou EVM, mais la tâche serait extrêmement difficile, et le résultat serait presque aussi difficile à vérifier. Au lieu de cela, avec Simplicity, nous avons défini un petit ensemble de combinateurs de base, chacun permettant, d’une manière fondamentale et mathématique, de combiner des fonctions. La sémantique du langage qui en résulte est si petite qu'elle tient sur un T-shirt.

En pratique, pour des choses comme l'inversion de bits, ce code ne sera écrit qu'une seule fois, puis réutilisé. En fait, nous avons fait le travail d'écriture pour vous et l'avons intégré au langage. Lorsque vous écrivez votre propre code, vous pouvez simplement utiliser le raccourci jet_not à la place du code ci-dessus. Nous reviendrons sur les jets dans la section suivante.

En fin de compte, dans la pratique, presque personne n'écrira de code Simplicity. Simplicity fournit une base bien définie pour les programmes de blockchain, mais ce n'est bien qu’une base. Le véritable travail sera effectué dans des langages de plus haut niveau, qui se compilent en code Simplicity avec des preuves de leur bon fonctionnement.

Programmes et expressions

Les expressions dont les valeurs d'entrée et de sortie sont triviales portent un nom particulier. Nous appelons ces expressions des programmes. D'un point de vue mathématique, il n'existe qu'une seule fonction qui associe une entrée triviale à une sortie triviale, il n'est donc pas évident que de telles expressions Simplicity soient utiles. Mais non seulement elles sont utiles, mais ce sont les seules expressions de ce type autorisées sur la blockchain !

Quelle est donc la stratégie ? Il y en a en fait deux : d'une part, les programmes Simplicity engagés dans les adresses comportent des trous, qui ne sont comblés que lorsque des jetons sont effectivement dépensées ; d'autre part, les programmes Simplicity ont des effets de bord, qui leur permettent d'accéder aux données de la blockchain ou de s'interrompre prématurément, permettant ainsi de dépasser les limites des fonctions mathématiques pures.

Il y a deux façons de spécifier des trous dans les programmes Simplicity : les combinateurs disconnect et witness. disconnect est un peu subtil, et nous en avons déjà parlé dans le passé. Les témoins sont quant à eux très simples : le combinateur witness retourne une valeur d'un type donné, appelé témoin, (comme une signature numérique, une préimage de hachage, ou un choix spécifique de clés de signature).

Simplicity supporte également les effets de bord de deux manières : l'une est l'introspection des données de transaction (dont nous parlerons plus en détail dans un article ultérieur), et l'autre est l'utilisation d'assertions. Les assertions arrêtent l'exécution du programme. Dans Bitcoin Script, l'opcode VERIFY est utilisé pour les assertions, et permet au programme d'échouer s'il rencontre une signature ou d'autres données invalides. EVM utilise l'opcode STOP dans le même but.

Nous pouvons maintenant voir comment un programme dont les types d'entrée et de sortie sont nominalement triviaux peut en fait effectuer un calcul utile : les témoins servent d'entrées au programme, tandis que les assertions fournissent une sortie de programme de type "réussite/échec".

Prenons un autre exemple. Voici un programme qui prend deux témoins et vérifie leur égalité :

-- Witnesses
wit1 := witness : 1 -> 2^32 
wit2 := witness : 1 -> 2^32 

-- Program code
pr1 := pair wit1 wit2 : 1 -> 2^64
jt2 := jet_eq_32      : 2^64 -> 2
cp3 := comp pr1 jt2   : 1 -> 2
jt4 := jet_verify     : 2 -> 1

main := comp cp3 jt4  : 1 -> 1

On peut lire ce programme de bas en haut : le programme lui-même est une expression unique appelée main, de type 1->1. Ici, le "type" d'expression indique le type de valeurs qu'elle prend en entrée et en sortie. Le type 1 n'a qu'une seule valeur et ne décrit donc aucune information. Le type 2 a deux valeurs possibles, il peut donc représenter un seul bit, 2^32 est une chaîne de 32 bits, et ainsi de suite.

D'après l'égalité du bas, nous voyons que main est la composition des expressions portant les noms cp3 et jt4. Ensuite, cp3 est lui-même la composition de pr1 et jt2, et ainsi de suite. Cinq combinateurs sont utilisés dans ce programme :

• comp, ou composition, prend deux expressions et évalue la seconde avec la sortie de la première comme entrée.
• pair prend deux expressions et produit une nouvelle expression dont la sortie est une paire de valeurs : la partie gauche est la sortie de la première expression, et la partie droite la sortie de la seconde.
• witness ne prend pas d'entrée mais a un type polymorphe comme sortie : quel que soit le type nécessaire pour que le programme ait un sens, c'est son type. La valeur qu'il produit est celle fournie au moment de l'évaluation.
• jet_eq_32 est un jet, ce qui signifie qu'il s'agit d'un combinateur unique qui remplace une expression Simplicity plus grande. L'expression remplacée est appelée sa spécification, et un interprète Simplicity peut évaluer le jet soit en évaluant la spécification, soit en utilisant du code machine optimisé qui a le même effet. Ce jet particulier prend deux valeurs de 32 bits et produit un seul bit, indiquant si les deux valeurs sont égales (1) ou inégales (0).
• jet_verify est également un jet. Celui-ci prend un seul bit en entrée, et si ce bit est à 0, il interrompt le programme. Il n'a pas de sortie.

Conclusion

Il s'agissait d'un article de blog dense dans lequel nous avons vu à quoi ressemble le code Simplicity, et observé que même une fonctionnalité d'apparence simple peut sembler assez complexe lorsqu'elle est écrite de manière explicite. Mais cette complexité reflète ce qui se passe réellement à l'intérieur. En tant que langage de spécification, Simplicity nous permet de tout rendre explicite, afin que nous puissions le modéliser mathématiquement, prouver les propriétés essentielles dont nous avons besoin pour nos applications, et ensuite l'encapsuler, confiant que nous avons une fondation solide pour notre code.

Simplicity possède plusieurs autres combinateurs et de nombreux jets, dont nous parlerons dans de prochains articles. Au fur et à mesure que nous construirons le langage, nous explorerons des exemples plus pratiques et nous verrons ce que signifie "prouver" des propriétés de programmes.

Mon prochain article présentera le concept de partage, qui permet de fusionner deux expressions identiques en une seule, et introduira quelques subtilités liées à la notion “d'identique".

Rejoignez les discussions sur Simplicity sur GitHub pour poser des questions, entrer en contact avec la communauté et partager vos idées. Et suivez-nous à @blksresearch sur Twitter pour rester au courant des dernières publications d’article de blog sur Simplicity.