Migration à partir de versions antérieures de Marlowe

Ce tutoriel explique comment la dernière version de Marlowe diffère des versions précédentes du langage.

Supprimer Both

Nous n'incluons pas la construction Both dans la dernière version de Marlowe, ce qui rend tous les contrats séquentiels.

Puisque dans aucune des versions de Marlowe il n'y a de communication entre les branches de Both, la seule fonctionnalité supplémentaire fournie par Both en pratique, c'était la possibilité d'attendre plusieurs dépôts d'argent en même temps.

Nous prenons en charge cette fonctionnalité en actualisant la construction When . Au lieu d'avoir des branches différentes qui attendent des entrées différentes, nous passons à un modèle complètement séquentiel et synchrone, où nous pouvons attendre une entrée parmi plusieurs possibles en même temps (comme dans select).

La raison pour laquelle nous avons supprimé cette construction est que les programmes séquentiels sont plus faciles à analyser et à raisonner, puisqu'il n'y a pas besoin de synchronisation et pas de possibilité de conditions de course.

Inclure les comptes

Dans les versions antérieures de Marlowe, chaque engagement a son propre timeout. Cela signifie que l'argent déposé dans un contrat n'est pas fongible, car il peut être distingué par son timeout. Pour obtenir la fongibilité, nous avons supprimé les timeouts des constructions individuelles, et avons un seul timeout pour tous les engagements. La durée de vie du contrat est facile à déduire à partir des timeouts dans le contrat.

Nous incluons cependant des comptes pour organiser l'argent déposé dans le contrat. Cela permet de rendre plus transparente la façon dont l'argent circule dans le contrat et, en particulier, d'identifier à qui l'argent est remboursé lorsque le contrat prend fin.

Chaque compte est identifié par un participant ; le participant indique qui obtiendra l'argent du compte par défaut lorsque Close est atteint.

La raison pour laquelle nous avons choisi d'inclure les comptes est que sans eux, nous avons constaté que nous devions essentiellement suivre les comptes manuellement. En outre, dans chaque feuille de l'AST, nous nous sommes retrouvés à calculer le montant que nous devions reverser à chaque participant, encombrant ainsi l'arbre d'un "texte passe-partout" répétitif. Ainsi, l'organisation de l'argent en comptes peut rendre les contrats plus faciles à raisonner et moins sujets à l'erreur.

Notez que nous pouvons assurer une fongibilité totale en utilisant un seul compte. Il nous suffit d'écrire les commandesPay appropriées dans les feuilles du contrat. Si tout l'argent est versé aux participants, alors Close n'a aucun effet. [1]

Discussion : Comptes implicites et comptes explicites

De nombreux cas d'utilisation des comptes - et tous ceux que nous pouvons identifier pour les contrats ACTUS - ont un compte par participant, et un participant par compte (le "modèle 1-1"). Cela soulève la question de savoir si nous devrions traiter implicitement les comptes, chaque participant possédant un compte.

D'autre part, il existe une variété de scénarios plausibles pour les comptes qui ne sont pas conformes au modèle 1-1.

Exemples de cas où plusieurs participants utilisent un compte.

Alice possède un compte sur lequel elle engage de l'argent pour que Bob le dépense (considérez Alice comme l'employeur de Bob). Bob peut dépenser jusqu'à la limite du compte, mais après l'expiration de l'engagement, Alice récupère tout ce qui reste.
Alice possède un compte sur lequel elle engage de l'argent pour que Bob et Carol le dépensent (considérez Alice comme l'employeur de Bob et Carol). Ils peuvent dépenser (conjointement) jusqu'à la limite du compte, mais après l'expiration de l'engagement, Alice récupère le solde.
D'un autre côté, on pourrait leur donner un compte séparé sur lequel ils pourraient dépenser : cela permettrait de faire respecter les limites individuelles ainsi qu'une limite globale.
Si Bob [et Carol] veulent dépenser de l'argent, ils peuvent aussi ajouter de l'argent sur le compte, mais ils doivent savoir que tout ce qui n'est pas utilisé sera remboursé à Alice.

Exemples de comptes multiples pour une même personne:

Des exemples de garantie pourraient convenir ici. Une personne souscrit un risque de premier niveau et un risque de second niveau en utilisant différents comptes. Ce n'est que lorsque la souscription de premier niveau de tous les participants est dépensée que les dépenses de second niveau sont effectuées.

Close remplace Null / Pay

Comme tous les contrats sont maintenant séquentiels, nous pouvons facilement dire quand un contrat prend fin, c'est-à-dire quand seulement Null reste. Nous profitons de cette occasion pour clôturer le contrat et rembourser l'argent restant sur les comptes ; c'est pourquoi nous avons renommé Null à Close (pour plus de clarté).

Comme indiqué précédemment, il n'y a plus de timeout explicite dans les comptes, puisque tous les contrats finiront par se réduire à Close. En fait, nous pouvons calculer statiquement et efficacement une limite supérieure pour le moment où cela se produira, ce qui rend cet aspect de Marlowe analysable.

Pay

Pay est maintenant immédiate, et elle a une seule continuation, et moins de paramètres. [2] Elle permet les paiements d'un compte à un participant ou à un autre compte. Nous avons écarté PayAll, puisqu'il peut être émulé comme une série finie de Pay. En fait, nous pouvons définir payAll comme une fonction Haskell (voir l'exemple de zeroCouponBond ).

La suppression de la construction Both a pour conséquence qu'il n'y a plus d'équivoque quant au premier Pay : ils sont tous séquentiels, ce qui facilite l'analyse. Avec la construction Both , nous pourrions potentiellement avoir des Pays dans n'importe quel ordre (puisque les deux côtés de Both sont censés fonctionner simultanément).

Multi-clause When

Nous avons modifié When pour inclure un ensemble d'actions possibles qui peuvent être saisies pendant que When attend. Nous appelons cette approche "Une parmi plusieurs", car elle accepte une action parmi les nombreuses actions potentiellement autorisées. When reste comme suit:

où When attendra le Timeout et continuera comme Contract, ou continuera comme spécifié dans l'un des Cases, selon ce qui se produit en premier. Case est défini comme suit:

et Action comme:

Une clause Case ne sera activée que si l' Action correspondante est produite, et elle se poursuivra en tant que Contract. En cas de concordance entre deux Actions , la première de la liste sera exécutée.

Trois types d'actions sont pris en charge:

Deposit représente un dépôt d'argent sur un compte ; il était à l'origine appelé Commit.
Choice représente un choix effectué par un participant parmi un ensemble de valeurs Integer (spécifiées par la liste des Bounds).
Notify attendra une action Notify émise lorsque l' Observation est vraie. Nous l'appelons Notify afin d'indiquer clairement que nous ne pouvons pas simplement attendre les Observations, mais que quelqu'un doit déclencher le contrat au moment où une Observation est vraie.

Nous avons éliminé l'ajout d'observations au Deposit et au Choice car il ne serait pas évident de savoir si l' Observation serait évaluée avant ou après l'application de l'action.

En plus des cas explicites dans When, nous devons nous rappeler que la branche timeout est aussi un cas, et qu'elle doit également être déclenchée (de manière similaire à Notify). [3] [4]

Observations et Values

Nous avons supprimé les Observations et les Values qui peuvent être exprimées en en combinant d'autres : comme AvailableMoney (pour l'ensemble du contrat), ou comme DepositedMoneyBy, qui se souvient du montant d'argent déposé par un participant, puisque le contrat peut être restructuré pour observer cela, et que le soutien nécessiterait des informations supplémentaires dans l'état (simplicité).

Nous avons conservé l'observation ChoseSomething même si, dans la sémantique proposée, chaque occurrence de ChoseSomething peut être évaluée statiquement et efficacement en examinant son contexte.

Par exemple, dans le contrat suivant, nous pouvons voir que la première occurrence de ChoseSomething sera évaluée à True, et la seconde à False:

Néanmoins, nous avons choisi de conserver cette construction pour deux raisons:

Il permet la réutilisation du code (commodité). Par exemple, dans le contrat précédent, nous pourrions définir chosen1:

Mais ceci ne serait pas possible si nous n'avions pas la construction ChoseSomething, puisque la valeur à laquelle elle se réduit dépend du contexte.

Il se peut que les occurrences de la construction ne puissent plus être évaluées de manière statique si nous étendons la construction When pour prendre en charge les entrées " plusieurs de plusieurs ".

Inclusion de SlotIntervals

La spécification EUTxO fournit des scripts de validation avec des intervalles de slot plutôt qu'avec des numéros de slot. Ceci a pour but de promouvoir le déterminisme dans les scripts de validation. Néanmoins, nous avons gardé le timeout de When (le seul timeout) comme un numéro de slot. La façon dont nous traitons les intervalles de slot est d'exiger que l'intervalle d'une transaction n'inclue pas de timeout sur lequel la sémantique doit faire un choix. Par exemple, si le timeout est de 10, une transaction avec un intervalle de 5 à 15 échouera avec AmbiguousSlotInterval. Les participants devront émettre une transaction avec l'intervalle 5-9 ou 10-15 (ou les deux).

Néanmoins, pour les Values, nous fournissons les deux constructions SlotIntervalStart et SlotIntervalEnd. Une alternative à considérer serait de modifier la sémantique pour que les valeurs soient non déterministes, de cette façon nous pourrions inclure une construction CurrentSlot et juste invalider les transactions qui sont ambiguës, mais cela compliquerait la sémantique et la rendrait moins prévisible.

[1]

Nous pouvons potentiellement fournir un moyen d'analyser statiquement le contrat pour vérifier s'il est possible qu'il reste de l'argent sur un compte lorsqueClose est atteint.

[2]

Cela signifie que les paiements obéissent maintenant à un modèle "push" plutôt qu'à un modèle "pull".

[3]

Néanmoins, le déclenchement du contrat pour le traitement des timeouts n'est pas urgent comme dans le cas de Notify, car tandis que les Observations peuvent alterner entre True et False, es timeouts ne peuvent se produire qu'une seule fois et, indépendamment du fait qu'ils aient été observés ou non par le contrat, ils ne peuvent pas être inversés.

[4]

En effet, un Case explicite ne peut plus être émis après le timeout, même si le timeout n'a pas été respecté par le contrat, puisque le timeout est vérifié avant les Inputs. Cependant, un participant peut vouloir déclencher un timeout dans les cas où aucun autre Inputs ne sont nécessaires, afin de déclencher un ou plusieurs paiements, par exemple. Dans l'implémentation actuelle de la sémantique, cela se fait en émettant une transaction avec une liste vide d' Inputs.

Vous trouverez une copie officielle de ce document ici :

https://alpha.marlowe.iohkdev.io/doc/marlowe/tutorials/migrating.html

https://docs.cardano.org/projects/plutus/en/latest/marlowe/tutorials/migrating.html

Plus de traductions de Cardano à: Cardano For The World