Los tipos de datos Marlowe

Este tutorial introduce formalmente a Marlowe como un tipo de datos de Haskell, además de presentar los diferentes tipos utilizados por el modelo, y discutir una serie de supuestos sobre la infraestructura en la que se ejecutarán los contratos. El código que describimos aquí proviene de los módulos Haskell Semantics.hs y Util.hs.

Marlowe

El lenguaje específico de dominio (DSL) de Marlowe se modela como una colección de tipos algebraicos en Haskell, con contratos dados por el tipo 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

En el tutorial anterior vimos lo que hacen estos contratos. En el resto de este tutorial profundizaremos un poco más en los tipos Haskell que se utilizan para representar los distintos componentes de los contratos, incluyendo cuentas, valores, observaciones y acciones. También veremos los tipos que se relacionan con la ejecución de los contratos, incluyendo las entradas, los estados, el entorno.

Componentes básicos

Para modelar las partes básicas de Marlowe utilizamos una combinación de Haskell data types, que definen nuevos types, y type sinónimos que dan un nuevo nombre a un existente type. [1]

Una Cuenta Marlowe contiene importes de múltiples monedas y/o tokens fungibles y no fungibles. Una cantidad concreta está indexada por un Token, que es un par de CurrencySymbol y TokenName. Puedes considerar un Account como un Map Token Integer, donde

data Token = Token CurrencySymbol TokenName

El token Ada de Cardano es Token adaSymbol adaToken. Pero puedes crear tus propias monedas y tokens.

Los tokens de una moneda pueden representar roles en un contrato, por ejemplo, "comprador" y "vendedor". Piensa en un contrato legal en el sentido de "en lo sucesivo, el ejecutante/vendedor/artista/consultor". De este modo, podemos desvincular la noción de propiedad de un rol contractual y hacer que sea negociable. Así, puedes vender tu préstamo o comprar una parte de un rol en algún contrato.

tradeRoles = CurrencySymbol "TradeRoles"

buyer = TokenName "buyer"

seller = TokenName "seller"

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

Aquí account tiene un buyer token de moneda "TradeRoles", y 1000 lovelace.

Un Party se representa como un hash de clave pública o un nombre de rol.

data Party = PK PubKeyHash | Role TokenName

Para hacer progresar un contrato Marlowe, una parte debe aportar una evidencia. Para parte PK esto sería una firma válida de una transacción firmada por una clave privada de una clave pública que tiene el hash del PubKeyHash de la parte, similar al mecanismo Pay to Public Key Hash de Bitcoin. Para una parte Role la evidencia es gastar un role token dentro de la misma transacción, normalmente al mismo propietario.

Así que, las partes Role se verán como (Role "alice"), (Role "bob") y así sucesivamente. Sin embargo, Haskell nos permite presentar y leer estos valores de forma más concisa (declarando una instancia personalizada de Show y utilizando overloaded strings) para que estos puedan ser introducidos y leídos como "alice", "bob" etc.

Los números de slot y las cantidades de dinero se tratan de forma similar; con el mismo esquema de show/overload aparecerán en los contratos como números:

data Slot = Slot Integer

type Timeout = Slot

Nota que "alice" es la propietaria en el sentido de que se le devolverá el dinero que haya en la cuenta cuando el contrato finalice.

Podemos utilizar overloaded strings para permitirnos abreviar esta cuenta por el nombre de su propietario: en este caso "alice".

Un pago puede hacerse a una de las partes del contrato, o a una de las cuentas del contrato, y esto se refleja en la definición

data Payee = Account Party

| Party Party

Las opciones -de números enteros- se identifican con ChoiceId que combina un nombre para la elección con el Party que ha hecho la elección:

type ChoiceName = Text

data ChoiceId = ChoiceId ChoiceName Party

type ChosenNum = Integer

Los valores, definidos mediante Let are also identified by integers. [2]

data ValueId = ValueId Integer

Values, observations and actions

Partiendo de los tipos básicos, podemos describir tres componentes de nivel superior de los contratos: un tipo de values, encima un tipo de observations, y también un tipo de actions, que desencadenan casos particulares. En primer lugar, observando a Value tenemos

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

Los diferentes tipos de values – que todos ellos son Integer – se explican por sí mismos, pero con el fin de estar completos, tenemos

Consulta del valor en una cuenta AvailableMoney, hecha en una elección ChoiceValue y en un identificador ya definido UseValue.
Constantes y operadores aritméticos.
Scale multiplica un Value por una constante racional, por ejemplo, 2/3, y redondea el resultado utilizando el redondeo " a medias " o " bancario ". Así, 14/10 se redondea a 1, tanto 15/10 como 25/10 se redondean a 2.
El inicio y el final del intervalo del slot actual; véase más abajo para más información sobre esto.
Cond representa las expresiones if, es decir, el primer argumento de Cond es una condición (Observation) para chequear, el segundo es un Value para tomar cuando la condición es satisfecha y el último es un Value para la condición insatisfecha; por ejemplo: (Cond FalseObs (Constant 1) (Constant 2)) es equivalente a (Constant 2)

A continuación tenemos 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

Son realmente autoexplicativos: podemos comparar valores para la (in)igualdad y la ordenación, y combinar observations utilizando las conectivas booleanas. La única otra construcción ChoseSomething indica si se ha hecho alguna elección para un determinado ChoiceId.

Los casos y las acciones vienen dados por estos tipos:

data Case = Case Action Contract

data Action = Deposit Party Party Token Value

| Choice ChoiceId [Bound]

| Notify Observation

data Bound = Bound Integer Integer

Tres tipos de actions son posibles:

Un Deposit n p t v hace un depósito de value v de token t de party p dentro de account n.
Se hace una elección para un id particular con una lista de límites en los valores que son aceptables. Por ejemplo, [Bound 0 0, Bound 3 5] ofrece la posibilidad de elegir una de las siguientes opciones 0, 3, 4 y 5.
El contrato es notificado para que se realice una determinada observación. Normalmente, esto lo haría una de las partes, o uno de sus wallets actuando automáticamente.

Esto completa nuestro análisis de los tipos que componen los contratos de Marlowe.

Transactions

Como hemos señalado anteriormente, la semántica de Marlowe consiste en la construcción de transacciones, así:

Una transacción se construye a partir de una serie de pasos, algunos de los cuales consumen un valor de entrada, y otros producen efectos, o pagos. Al describir esto explicamos que una transacción modificaba un contrato (a su continuación) y el estado, pero más precisamente tenemos una función

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

donde los tipos se definen así:

data TransactionInput = TransactionInput

{ txInterval :: SlotInterval

, txInputs :: [Input] }

data TransactionOutput =

TransactionOutput

{ txOutWarnings :: [ReduceWarning]

, txOutPayments :: [Payment]

, txOutState :: State

, txOutContract :: Contract }

| Error TransactionError

La notación utilizada aquí añade los nombres de los campos a los argumentos de los constructores, proporcionando selectores para los datos, así como haciendo más claro el propósito de cada campo.

El tipo TransactionInput tiene dos componentes: el SlotInterval en el que puede añadirse válidamente a la blockchain, y una secuencia ordenada de valores de Input que se procesarán en esa transacción.

Un value TransactionOutput tiene cuatro componentes: los dos últimos son el State y el Contract actualizados, mientras que el segundo da una secuencia ordenada de Payments producidos por la transacción. El primer componente contiene una lista de las advertencias producidas por el procesamiento de la transacción.

Series de slots

Esto forma parte de la arquitectura de Cardano/Plutus, que reconoce que no es posible predecir con precisión en qué slot se procesará una transacción concreta. Por lo tanto, a las transacciones se les da un intervalo de slots en el que se espera que se procesen, y esto se traslada a Marlowe: cada paso de un contrato de Marlowe se procesa en el contexto de una serie de slots.

data Slot = Slot Integer

data SlotInterval = SlotInterval Slot Slot

ivFrom, ivTo :: SlotInterval -> Slot

ivFrom (SlotInterval from _) = from

ivTo (SlotInterval _ to) = to

¿Cómo afecta esto al procesamiento de un contrato Marlowe? Cada paso se procesa en relación con un intervalo de slots, y el valor del slot actual tiene que estar dentro de ese intervalo.

Los puntos finales del intervalo son accesibles como los valores SlotIntervalStart y SlotIntervalEnd, y estos pueden ser utilizados en las observaciones. Los timeouts deben procesarse de forma inequívoca, de modo que todos los valores del intervalo de slots tienen que haber superado el timeout para que surta efecto, o caer antes del timeout, para que la ejecución normal surta efecto. En otras palabras, el valor del timeout debe ser menor o igual que SlotIntervalStart (para que el timeout tenga efecto) o ser estrictamente mayor que SlotIntervalEnd (para que la ejecución normal tenga lugar).

Notas

El modelo hace una serie de suposiciones sobre la infraestructura de blockchain en la que se ejecuta.

Se supone que las funciones y operaciones criptográficas son proporcionadas por una capa externa a Marlowe, por lo que no es necesario modelarlas explícitamente.
Suponemos que el tiempo es de "grano grueso" y se mide por número de bloque o slot, de modo que, en particular, los timeouts se delimitan utilizando números de bloque/slot.
La realización de un depósito no es algo que un contrato pueda llevar a cabo; más bien, puede solicitar que se realice un depósito, pero eso entonces tiene que establecerse externamente: de ahí la entrada de (una colección de) depósitos para cada transacción.
El modelo administra la devolución de fondos al propietario de una cuenta particular cuando un contrato alcanza el punto de Close.

[1]

De hecho, utilizamos declaraciones newtype en vez de data types porque se implementan de manera más eficiente.

[2]

Esto puede ser modificado en el futuro para permitir que los valores sean nombrados por strings.

Encuentra una copia oficial de este documento aquí:

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

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

Más traducciones de Cardano en: Cardano For The World