Traducción al español de “Actus smart contracts in Marlowe”
Publicado por Prof Simon Thompson en el blog de IOHK el 13 de Octubre de 2020
Escribir en el lenguaje de las finanzas, en lugar del lenguaje blockchain
En nuestra serie de blogs técnicos ocasionales “Developer Deep Dive”, invitamos a los investigadores e ingenieros de IOHK a discutir sus últimos trabajos y conocimientos.
Marlowe es un lenguaje de dominio específico para contratos inteligentes financieros seguros que está siendo desarrollado por IOHK para las capacidades Goguen de la blockchain Cardano. Después de mi post introductorio sobre Marlowe, en este post de Deep Dive, veremos los detalles del lenguaje, y las diversas formas de escribir contratos inteligentes Marlowe a medida que avanzamos en la era de las finanzas descentralizadas (DeFi). Después de explicar nuestro enfoque de oráculos, que importan la información del “mundo real” en un contrato en curso, veremos el Estándar Unificado de Tipos de Contratos Algorítmicos (Actus) para los contratos financieros, y explicaremos cómo hemos implementado esta innovación en Marlowe.
Marlowe en pocas palabras
Marlowe es un lenguaje pequeño, con un puñado de construcciones que, para cada contrato, describen un comportamiento que implica un conjunto fijo y finito de roles.
- Un contrato en ejecución puede hacer un pago a un rol o a una clave pública.
- De manera complementaria, un contrato puede esperar una acción de uno de los roles, como un depósito de dinero, o una elección de un conjunto de opciones. De manera crucial, un contrato no puede esperar indefinidamente: si no se ha iniciado ninguna acción en un momento determinado (el límite de tiempo), entonces el contrato continuará con otro comportamiento, como el reembolso de los fondos del contrato.
- Dependiendo del estado actual de un contrato, puede elegir entre dos cursos de acción futuros, que son en sí mismos contratos.
- Cuando no se requieran más acciones, el contrato se cerrará, y se devolverá cualquier dinero restante en el contrato.
Cuando se ejecuta un contrato, los roles que implica son cumplidos por los participantes, que son identidades en la blockchain. Este modelo permite transferir un rol durante la ejecución del contrato, de modo que los roles en un contrato en curso pueden ser intercambiados. Cada rol está representado por un token en la cadena, y al transferirla se transfiere la capacidad de realizar las acciones del papel. Llevando esto más allá, podemos representar un único rol con múltiples tokens, permitiendo así que el rol sea compartido: esto podría denominarse ser “securitizado”.
El sistema Marlowe
Hemos elegido deliberadamente hacer el lenguaje lo más simple posible, para que sea fácil de implementar en Cardano y en el Playground Marlowe. Marlowe describe el flujo de criptomonedas entre los participantes, y para que esto se implemente en la práctica en la blockchain Cardano, el código tiene que ser ejecutado tanto en la cadena como fuera de ella: recuerden, sin embargo, que sólo un contrato Marlowe describe ambas partes. La parte en cadena acepta y valida las transacciones que se ajustan a los requisitos del contrato inteligente: esta parte se implementa como un único guión de Plutus para todos los contratos Marlowe, y el contrato Marlowe en particular comprende un dato que se pasa a través de las transacciones. Fuera de la cadena, el contrato Marlowe se presentará a través de la interfaz de usuario y la billetera, ofreciendo o, de hecho, automatizando los depósitos y las elecciones y recibiendo pagos en criptomonedas.
Figura 1. El Playground Marlowe simula las formas en que los contratos se comportan
En el Playground podemos simular el comportamiento de los contratos, de modo que los usuarios potenciales pueden caminar a través de diferentes formas en que los contratos evolucionarán, de acuerdo a las diferentes acciones tomadas por los participantes. En la simulación principal, la figura 1, los usuarios tienen un punto de vista omnisciente y son capaces de realizar acciones por cualquier participante, con la opción en cada punto de deshacer las acciones tomadas, y luego tomar un camino diferente. La simulación de la billetera permite a los usuarios ver el comportamiento desde la perspectiva de un participante en particular, simulando así cómo ese usuario interactuará con el contrato de ejecución una vez que se despliega en la blockchain.
Esta simplicidad también nos permite modelar los contratos Marlowe en un solucionador SMT, un sistema lógico para comprobar automáticamente las propiedades de los sistemas. Utilizando este modelo, que llamamos análisis estático, para cada contrato somos capaces de comprobar si puede o no fallar en el cumplimiento de un pago, y si el contrato puede fallar obtenemos evidencias de cómo falla, ayudando al autor a reescribir el contrato si lo desea.
Podemos construir un modelo formal de nuestra implementación en un asistente de pruebas, en el que somos capaces de producir pruebas verificadas por máquina de cómo se comporta el lenguaje. Mientras que el solucionador SMT funciona para contratos individuales, el asistente de pruebas puede probar las propiedades de las plantillas de contratos, así como el propio sistema: por ejemplo, podemos mostrar que en cualquier contrato en curso, las cuentas a las que hace referencia nunca pueden estar en débito. La simulación, el análisis estático y la prueba proporcionan niveles complementarios de garantía para un contrato en el que los usuarios comprometerán activos para asegurar que el contrato se comporte como debe.
Escribiendo contratos Marlowe
Hemos visto cómo los contratos Marlowe pueden ser analizados de varias maneras, pero ¿cómo escriben realmente los autores contratos inteligentes en Marlowe? El Playground proporciona varias formas de producir contratos Marlowe. Los usuarios pueden escribir Marlowe directamente, pero los principiantes a menudo optan por construir los contratos visualmente, utilizando un editor interactivo Blockly. La figura 2 muestra una sección de un contrato de depósito en garantía.
Figura 2. Un contrato de depósito en garantía en el editor interactivo Blocky del Playground
Trabajar en este editor visual tiene la ventaja de mostrar todas las opciones al seleccionar cómo rellenar una parte del contrato que se está desarrollando. Alternativamente, puedes desarrollar contratos en Haskell, porque el DSL Marlowe está de hecho incrustado en Haskell. La figura 3 muestra el mismo contrato en Haskell: las partes azules y púrpuras son de Marlowe, y los componentes negros están definidos en Haskell, como abreviaturas que hacen más legible el contrato general. Este enfoque permite a los usuarios construir un contrato inteligente paso a paso a partir de los componentes. En el código que se muestra en la figura 3, se pide a los roles, Alice y Bob, que hagan una elección: si sus elecciones coinciden, están de acuerdo, y el contrato procede de una manera; si no, entonces se pide a un tercer participante, Carol, que arbitre entre ellos. El acuerdo de los contratos y el arbitraje se definen más adelante en el archivo de Haskell.
Figura 3. El contrato de depósito en garantía en Haskell
Los usuarios también podrán escribir sus contratos financieros inteligentes utilizando JavaScript, mientras que siguen disfrutando de todas las ventajas del análisis, la simulación y la prueba, tal y como se prevé en la implementación de Marlowe.
Oráculos
Una de las primeras preguntas que nos hacen cuando describimos Marlowe es sobre los oráculos financieros, o cómo podemos conseguir que un contrato tenga en cuenta los valores de los datos externos, como el tipo de cambio entre ada y bitcoin. En resumen, un oráculo es como un participante que hace una elección, y así la semántica de Marlowe ya puede tratar con valores externos. Sin embargo, planeamos apoyar los valores del oráculo como parte de la implementación, permitiendo que los contratos accedan a los valores directamente desde un teletipo de la bolsa o un alimentador de datos como Coinbase. Al mismo tiempo, el equipo de Plutus está investigando la mejor manera de tratar con los oráculos en general, y podemos esperar apoyo para eso a su debido tiempo, aunque tal vez no en la primera versión completa de Marlowe y el Marco de Aplicación de Plutus.
Actus para contratos financieros
Marlowe tiene el potencial de dar a la gente la oportunidad de hacer compromisos financieros y comerciar sin que un tercero lo facilite: la blockchain asegura que el contrato se cumpla.
Estamos construyendo una implementación Marlowe de contratos desintermediados para ofrecer a los usuarios finales que quieran hacer tratos financieros entre iguales directamente sin la intervención de terceros.
La Fundación de Investigación Financiera Actus categoriza los contratos financieros mediante una taxonomía que se describe en una especificación técnica detallada.
Actus se basa en el entendimiento de que los contratos financieros son acuerdos legales entre dos (o más) contrapartes sobre el intercambio de futuras corrientes de efectivo. Históricamente, esos acuerdos jurídicos se describen en lenguaje natural, lo que da lugar a una ambigüedad y una diversidad artificial. Como respuesta, Actus define los contratos mediante un conjunto de términos contractuales y funciones determinantes que asignan esos términos a las obligaciones de pago futuras. De este modo, es posible describir la mayoría de los instrumentos financieros mediante 31 tipos de contratos o plantillas modulares.
A continuación, examinamos un ejemplo sencillo y luego explicamos nuestro enfoque completo de la aplicación de Actus, con enfoques complementarios que ofrecen diferentes ventajas y desventajas.
Un primer ejemplo de Actus
Un bono de cupón cero es un título de deuda que no paga intereses (un cupón) pero que se emite con un descuento, lo que permite obtener beneficios al vencimiento cuando el bono se amortiza por su valor nominal completo.
Por ejemplo, la figura 4 describe un contrato por el que un inversor puede comprar un bono que cuesta 1.000 lovelaces con un 15% de descuento. Paga 850 lovelaces al emisor del bono antes de la hora de inicio, aquí franja 10.
Más tarde, después de la fecha de vencimiento, franja 20 aquí, el inversor puede cambiar el bono por su valor nominal completo, es decir, 1.000 lovelaces.
Figura 4. Contrato de un bono de cupón cero con un 15% de descuento
Este contrato tiene un inconveniente importante. Una vez que el inversor haya depositado los 850 lovelaces, se pagará inmediatamente al emisor; si el inversor no invierte con la suficiente rapidez, es decir, antes del tiempo de espera, el contrato termina. Después de eso, hay dos resultados posibles:
- el emisor deposita 1.000 lovelaces en la cuenta del inversor, y esa suma se paga inmediatamente al inversor en su totalidad;
- si el inversor no hace el depósito, entonces el contrato se cierra y todo el dinero del contrato se devuelve, pero no hay dinero en el contrato en este momento, por lo que el inversor pierde su dinero.
¿Cómo podemos evitar este problema de que el emisor de bonos no cumpla con su obligación? Hay al menos dos maneras de resolverlo: podríamos pedirle al emisor que deposite la cantidad total antes de que comience el contrato, pero eso frustraría el objeto de la emisión del bono en primer lugar. Más realista, podríamos pedir a un tercero que sea garante del acuerdo, como se expresa aquí.
Figura 5. Mejora del contrato con un garante
Actus en Marlowe
Los productos de la taxonomía Actus, como el contrato de capital a vencimiento, pueden presentarse de diferentes maneras en Marlowe, según el grado en que puedan aceptar cambios en sus términos durante la vigencia del contrato (figura 6).
Figura 6. Taxonomía Actus y Marlowe
En el caso más sencillo, todas las corrientes de efectivo se fijan, o congelan, al inicio del contrato, de modo que es totalmente previsible cómo funcionará el contrato, suponiendo que todos los participantes sigan participando en él durante su vigencia. Los contratos de este tipo los llamamos Actus-F (para fijos o congelados).
El dinamismo, es decir, el cambio durante la evolución del contrato, puede ocurrir de dos maneras. Los participantes pueden hacer pagos no programados que requieren un nuevo cálculo de los flujos de caja restantes, y también los flujos de caja pueden modificarse teniendo en cuenta factores de riesgo externos. La generalidad completa de los contratos que hacen ambas cosas se modelan en Actus-M (para Marlowe).
También hay niveles intermedios: Los modelos de Actus-FS tienen calendarios fijos: permiten tener en cuenta los factores de riesgo, pero sin pagos inesperados; por el contrario, los contratos de Actus-FR permiten realizar pagos en puntos inesperados, pero no tienen en cuenta ningún factor de riesgo.
Por último, saliendo de Marlowe, Actus-H (H de Haskell) modela los contratos directamente como programas en Plutus o Haskell, utilizando Marlowe para la validación de cada transacción en la vida del contrato, generando el código Plutus a partir de la descripción de Marlowe de la lógica del contrato.
¿Por qué ofrecemos estos diferentes modelos de contratos de Actus? La razón es que hay un equilibrio entre la naturaleza dinámica de los contratos y la garantía que podemos dar a los usuarios sobre la forma en que se ejecutarán los contratos antes de su ejecución.
-
Los contratos Actus-F presentan un calendario de pagos totalmente fijo, que puede ser examinado directamente por los participantes para que sea sencillo ver, por ejemplo, que todos los pagos de un contrato de este tipo tendrán éxito.
-
Los contratos Actus-FS y -FR presentan un mayor dinamismo, pero los contratos son legibles y fáciles de escrutar. Además, están sujetos a un análisis estático (más lento) para establecer, por ejemplo, que todos los pagos tendrán éxito.
-
Los contratos Actus-M están expresados en Marlowe, por lo que pueden ser analizados. Sin embargo, el análisis es sustancialmente más lento debido a la imprevisibilidad de las acciones que el contrato sufrirá en un momento determinado. Obsérvese que se puede ofrecer una garantía para las versiones reducidas de los contratos, que tienen el mismo contenido computacional, pero que evolucionan en un tiempo más corto, lo que implica menos interacciones.
-
Los contratos Actus-H están redactados en una combinación de Plutus y Marlowe, por lo que no son susceptibles de verificación estática de la misma manera que los demás. Sin embargo, esta plataforma ofrece a los clientes empresariales una total extensibilidad y adaptación de la aplicación de la norma Actus.
En nuestra implementación de Actus, disponible como versión previa al lanzamiento en la pestaña Laboratorios del Playground, los usuarios pueden generar contratos Actus-F y -FS a partir de los términos del contrato, utilizando una presentación visual de los datos requeridos.
Figura 7. Los tres elementos con asteriscos se requieren para un contrato de capital a vencimiento
Para un contrato de capital a vencimiento, se requieren tres elementos: la fecha de inicio y de finalización, y el importe teórico del contrato (de ahí que los elementos se destaquen en la plantilla). Dicho contrato comprenderá una carga simple, en la que el importe nocional se transfiere de la contraparte a la parte al inicio del contrato, y en sentido inverso en la fecha de vencimiento.
La adición de elementos adicionales modificará el contrato generado en consecuencia. En la figura 7, la parte tendrá que transferir el nocional más la prima a la contraparte en la fecha de vencimiento, dando así a la contraparte un incentivo para hacer el préstamo en primer lugar.
Entrando en un mundo DeFi con contratos inteligentes
Como hemos visto, los profesionales de las finanzas y los desarrolladores ahora tienen una manera de empezar a crear contratos inteligentes financieros directamente en Haskell o en Marlowe puro, o visualmente, usando el Playground Marlowe, dependiendo de su experiencia en programación. En el Playground se pueden simular y analizar los contratos que se crean para comprobar que funcionan correctamente y que están listos para ser emitidos en el mundo de las finanzas descentralizadas cuando se implemente la etapa Goguen de Cardano. El equipo Marlowe de IOHK continuará implementando ejemplos de la norma Actus, mientras nos preparamos para finalizar la implementación de Marlowe en Cardano, y llevar los contratos financieros inteligentes a la propia blockchain.