Analyse statique

Un trait distinctif de Marlowe - probablement son trait le plus distinctif - est que nous pouvons analyser les contrats, et en déduire des propriétés, sans les exécuter.

Nous pouvons vérifier, avant d'exécuter un contrat, ces propriétés:

Paiements partiels : c'est-à-dire des paiements lorsqu'il n'y avait pas assez d'argent sur le compte.
Dépôts non positifs : dans le cadre desquels le contrat demande une valeur négative ou nulle.
Paiements non positifs : paiements de 0 ou d'un montant négatif.
Ombrage de Lets , où deux Lets définissent le même identifiant dans le même chemin d'exécution.

Dans la suite de ce tutoriel, nous allons nous concentrer sur la première de ces erreurs, qui est la pire. C'est dans ce cas qu'un paiement échoue, car il n'y a pas assez d'argent dans le contrat (ou plus strictement sur le compte) pour effectuer un paiement complet.

Un exemple

Examinons cet exemple, dans Blockly

Et en pur Marlowe

Le contrat exige d'abord un dépôt d'Alice de 1 Lovelace, et demande ensuite à Bob de faire un choix (appelé bool) de 0 ou 1. Le contrat paie ensuite ce choix plus un à Bob à partir du compte d'Alice.

Donc, nous pouvons voir que, bien que le contrat fonctionne correctement lorsque Bob choisit 0, il n'y aura pas assez dans le contrat pour lui payer s'il choisit 1. Notre analyse, qui est intégrée dans l'onglet SIMULATION du Marlowe Playground, peut diagnostiquer ce problème:

Cela montre que l'erreur se produit lorsque

Alice a fait le dépôt, et
Bob a choisi la valeur 1.

et que l'erreur générée est une TransactionPartialPay: dans ce cas, Bob reçoit seulement un paiement de 1 au lieu de 2.

Si nous modifions le contrat de façon à ce qu'Alice fasse un dépôt initial de 2, alors l'analyse réussira:

Sous le capot

Je le répète : cette analyse a pour effet de vérifier tous les chemins d'exécution possibles du contrat, en utilisant une version symbolique du contrat. Cette version est transmise au solveur Z3 SMT, qui est un système automatisé de pointe permettant de déterminer si les formules logiques sont satisfaisables.

Si l'analyse n'aboutit pas, c'est-à-dire s'il existe un moyen de faire échouer le paiement du contrat, le système donne également un exemple de la manière dont cela peut se passer et le présente à l'utilisateur. L'utilisateur peut alors corriger le problème et le vérifier à nouveau.

Prochains pas

Au cours des prochains mois, nous examinerons comment présenter les résultats de notre analyse d'une manière plus "sympa", et nous élargirons la portée de notre travail.

Utilisez le bouton d'analyse dans le Marlowe Playground pour analyser certains des contrats que vous avez déjà rédigés. Si l'analyse échoue, pouvez-vous voir pourquoi et corriger les contrats pour qu'ils n'échouent pas ?

Vous trouverez une copie officielle de ce document ici :

https://alpha.marlowe.iohkdev.io/doc/marlowe/tutorials/static-analysis.html

https://docs.cardano.org/projects/plutus/en/latest/marlowe/tutorials/static-analysis.html

Plus de traductions de Cardano à: Cardano For The World