Les types de données Marlowe

Ce tutoriel introduit formellement Marlowe en tant que type de données Haskell, tout en présentant les différents types utilisés par le modèle et en discutant un certain nombre d'hypothèses sur l'infrastructure dans laquelle les contrats seront exécutés. Le code que nous décrivons ici provient des modules Haskell Semantics.hs et Util.hs.

Marlowe

Le langage spécifique au domaine (DSL) Marlowe est modélisé comme une collection de types algébriques en Haskell, les contrats étant donnés par le type Contract :

data Contract = Close

| Pay Party Payee Token Value Contract

| If Observation Contract Contract

| When [Case] Timeout Contract

| Let ValueId Value Contract

| Assert Observation Contract

Nous avons vu dans le tutoriel précédent ce que font ces contrats. Dans la suite de ce tutoriel, nous allons approfondir les types Haskell utilisés pour représenter les différents composants des contrats, notamment les comptes, les valeurs, les observations et les actions. Nous examinerons également les types relatifs à l'exécution des contrats, notamment les entrées, les états, l'environnement, etc.

Composants de base

Dans la modélisation des parties de base de Marlowe, nous utilisons une combinaison de Haskell data types, qui définissent des nouveaux types, et type synonymes qui donnent un nouveau nom à un existant type. [1]

Un compte Marlowe contient des montants en devises multiples et/ou en tokens fongibles et non fongibles. Un montant concret est indexé par un Token, qui est une paire de CurrencySymbol et TokenName. Vous pouvez considérer un compte comme un Map Token Integer, où

data Token = Token CurrencySymbol TokenName

Le token Ada de Cardano est Token adaSymbol adaToken. Mais vous êtes libre de créer vos propres monnaies et tokens.

Les tokens d'une monnaie peuvent représenter des rôles dans un contrat, par exemple "acheteur" et "vendeur". Pensez à un contrat légal dans le sens de "ci-après dénommé l'exécutant/vendeur/artiste/consultant". De cette façon, nous pouvons découpler la notion de propriété d'un rôle de contrat et le rendre échangeable. Ainsi, vous pouvez vendre votre prêt ou acheter une part d'un rôle dans un certain contrat.

tradeRoles = CurrencySymbol "TradeRoles"

buyer = TokenName "buyer"

seller = TokenName "seller"

account = fromList[(Token tradeRoles buyer, 1), (ada 1000)]

Ici account tient un buyer token de la monnaie "TradeRoles", et 1000 lovelace.

Un Party est représenté soit par un hash de clé publique, soit par un nom de rôle.

data Party = PK PubKeyHash | Role TokenName

Afin de faire progresser un contrat Marlowe, une partie doit fournir une évidence. Pour la partie PK ceci serait une signature valide d'une transaction signée par une clé privée d'une clé publique qui est hachée à la PubKeyHash de la partie, similaire au mécanisme Pay to Public Key Hash de Bitcoin. Pour une partie Role l'évidence est de dépenser un role token au cours d'une même transaction, généralement au profit du même propriétaire.

Alors, les parties Role apparaîtront comme suit (Role "alice"), (Role "bob") et ainsi de suite. Cependant, Haskell nous permet de présenter et de lire ces valeurs de manière plus concise (en déclarant une instance personnalisée de Show et en utilisant des overloaded strings) de sorte que celles-ci puissent être entrées et lues comme "alice", "bob" etc.

Les numéros de slot et les montants d'argent sont traités de manière similaire ; avec la même approche de show/overload, ils apparaîtront dans les contrats comme des numéros:

data Slot = Slot Integer

type Timeout = Slot

Notez que "alice" est la propriétaire dans le sens qu'elle sera remboursée toute l'argent sur son compte à la fin du contrat.

Nous pouvons utiliser des overloaded strings pour nous permettre d'abréger ce compte par le nom de son propriétaire : dans ce cas, il s'agit de "alice".

Un paiement peut être fait à l'une des parties au contrat, ou à l'un des comptes du contrat, et cela se reflète dans la définition

data Payee = Account Party

| Party Party

Les choix - d'entiers - sont identifiés par ChoiceId qui combine un nom pour le choix avec le Party qui a fait le choix:

type ChoiceName = Text

data ChoiceId = ChoiceId ChoiceName Party

type ChosenNum = Integer

Valeurs, telles que définies par Let sont également identifiées par des entiers. [2]

data ValueId = ValueId Integer

Values, observations et actions

À partir des types de base, nous pouvons décrire trois composantes de plus haut niveau des contrats : un type de values, un type d'observations et un type d'actions, qui déclenchent des cas particuliers. Tout d'abord, en regardant à Value on a

data Value = AvailableMoney Party Token

| Constant Integer

| NegValue Value

| AddValue Value Value

| SubValue Value Value

| MulValue Value Value

| Scale Rational Value

| ChoiceValue ChoiceId

| SlotIntervalStart

| SlotIntervalEnd

| UseValue ValueId

| Cond Observation Value Value

Les différents types de values - qui sont tous Integer – sont assez explicites, mais pour être complet nous avons

Consultation de la valeur d'un compte AvailableMoney, faite dans un choix ChoiceValue et dans un identifiant qui a déjà été défini UseValue.
Constantes et opérateurs arithmétiques.
Scale multiplie une Value par une constante rationnelle, par exemple 2/3, et arrondit le résultat en utilisant l'arrondi "demi-pair" ou "bancaire". Ainsi, 14/10 est arrondi à 1, 15/10 et 25/10 sont arrondis à 2..
Le début et la fin de l'intervalle du slot en cours ; voir ci-dessous pour plus de détails à ce sujet.
Cond représente des expressions if, c'est-à-dire - le premier argument de Cond est une condition (Observation) à vérifier, le second est un Value à prendre lorsque la condition est satisfaite et le dernier est un Value pour une condition non satisfaite ; par exemple: (Cond FalseObs (Constant 1) (Constant 2)) est equivalent à (Constant 2)

Ensuite, nous avons observations

data Observation = AndObs Observation Observation

| OrObs Observation Observation

| NotObs Observation

| ChoseSomething ChoiceId

| ValueGE Value Value

| ValueGT Value Value

| ValueLT Value Value

| ValueLE Value Value

| ValueEQ Value Value

| TrueObs

| FalseObs

Ces constructions sont vraiment explicites : nous pouvons comparer des valeurs pour l'(in)égalité et l'ordre, et combiner des observations en utilisant les connecteurs booléens. La seule autre construction ChoseSomething indique si un choix a été fait pour un ChoiceId.

Les cas et les actions sont donnés par ces types:

data Case = Case Action Contract

data Action = Deposit Party Party Token Value

| Choice ChoiceId [Bound]

| Notify Observation

data Bound = Bound Integer Integer

Trois types de action sont possibles:

Un Deposit n p t v fait un dépôt de value v de token t de party p dans account n.
Un choix est fait pour un id particulier avec une liste de limites sur les valeurs qui sont acceptables. Par exemple, [Bound 0 0, Bound 3 5] offre le choix entre 0, 3, 4 et 5.
Le contrat est notifié qu'une observation particulière doit être faite. En général, cette observation est effectuée par l'une des parties ou par l'un de leurs wallets agissant automatiquement.

Ceci termine notre discussion sur les types qui composent les contrats de Marlowe.

Transactions

Comme nous l'avons noté précédemment, la sémantique de Marlowe consiste à construire des transactions, comme ceci:

Une transaction est construite à partir d'une série d'étapes, dont certaines consomment une valeur d'entrée, et d'autres produisent des effets, ou des paiements. En décrivant cela, nous avons expliqué qu'une transaction modifiait un contrat (à sa suite) et l'état, mais plus précisément nous avons une fonction

computeTransaction :: TransactionInput -> State -> Contract -> TransactionOutput

où les types sont définis comme suit:

data TransactionInput = TransactionInput

{ txInterval :: SlotInterval

, txInputs :: [Input] }

data TransactionOutput =

TransactionOutput

{ txOutWarnings :: [ReduceWarning]

, txOutPayments :: [Payment]

, txOutState :: State

, txOutContract :: Contract }

| Error TransactionError

La notation utilisée ici ajoute des noms de champs aux arguments des constructeurs, ce qui permet de sélectionner les données et de clarifier l'objectif de chaque champ..

Le typeTransactionInput a deux composantes : le SlotInterval dans lequel elle peut être valablement ajoutée à la blockchain, et une séquence ordonnée de valeurs Input à traiter dans cette transaction.

Une valeur TransactionOutput a quatre composants : les deux derniers sont le State et le Contract mis à jour, tandis que le second donne une séquence ordonnée de Payments produits par la transaction. Le premier composant contient une liste de tous les avertissements produits par le traitement de la transaction.

Séries de slots

Cela fait partie de l'architecture de Cardano/Plutus, qui reconnaît qu'il n'est pas possible de prédire précisément dans quel slot une transaction particulière sera traitée. Les transactions se voient donc attribuer un intervalle de slots dans lequel elles sont censées être traitées, ce qui se répercute sur Marlowe : chaque étape d'un contrat Marlowe est traitée dans le contexte d'une série de slots.

data Slot = Slot Integer

data SlotInterval = SlotInterval Slot Slot

ivFrom, ivTo :: SlotInterval -> Slot

ivFrom (SlotInterval from _) = from

ivTo (SlotInterval _ to) = to

Comment cela affecte-t-il le traitement d'un contrat Marlowe ? Chaque étape est traitée par rapport à un intervalle de slot, et la valeur actuelle du slot doit être comprise dans cet intervalle.

Les extrémités de l'intervalle sont accessibles comme les valeurs SlotIntervalStart et SlotIntervalEnd, et ceux-ci peuvent être utilisés dans les observations. Les timeouts doivent être traités sans ambiguïté, de sorte que toutes les valeurs dans l'intervalle de slot doivent soit avoir dépassé le timeout pour qu'il prenne effet, soit tomber avant le timeout, pour que l'exécution normale prenne effet. En d'autres termes, la valeur du timeout doit être soit inférieure ou égale à SlotIntervalStart (pour que le timeout prenne effet) ou être strictement supérieur à SlotIntervalEnd (pour que l'exécution normale ait lieu).

Notes

Le modèle fait un certain nombre de suppositions sur l'infrastructure blockchain dans laquelle il est exécuté.

Il est supposé que les fonctions et opérations cryptographiques sont fournies par une couche externe à Marlowe, et qu'il n'est donc pas nécessaire de les modéliser explicitement.
Nous supposons que le temps est "à gros grains" et qu'il est mesuré par le numéro de bloc ou de slot, de sorte que, en particulier, les timeouts sont délimités à l'aide des numéros de bloc/slot.
Effectuer un dépôt n'est pas quelque chose qu'un contrat peut faire ; il peut plutôt demander qu'un dépôt soit effectué, mais cela doit alors être établi de l'extérieur : d'où l'introduction de (une collection de) dépôts pour chaque transaction.
Le modèle gère le remboursement des fonds au propriétaire d'un compte particulier lorsqu'un contrat atteint le point de Close.

[1]

En fait, on a utilize des declarations newtype au lieu de data types parce qu'ils sont implémentés de manière plus efficace.

[2]

Ceci peut être modifié dans le futur pour permettre aux valeurs d'être nommées par des strings.

Vous trouverez une copie officielle de ce document ici :

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

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

Plus de traductions de Cardano à: Cardano For The World