🇪🇸 Marlowe 9: verificando los contratos Marlowe

:es: Traducción al español de “Marlowe 9: verifying Marlowe contracts”

Publicado en el canal de Youtube de Simon Thompson el 16 de Abril de 2020

Enlace a la versión doblada al español


En este video me gustaría hablar un poco sobre cómo podemos verificar que los contratos Marlowe se comportan como deberían, al principio dije, cuando hablamos de lenguajes de dominio específico, que debido a que estamos trabajando en un lenguaje más específico, podemos hacer más con él y este es un punto en el que puedo cumplir esa promesa. Así que lo primero de lo que quiero hablar es lo que se llama análisis estático, lo que quiero decir con eso es que podemos analizar el comportamiento completo de un contrato Marlowe, un contrato Marlowe específico, completamente sin ejecutarlo, es completamente automático, así que no hay necesidad de que los usuarios hagan cualquier cosa y es exhaustivo, comprueba todas las partes posibles a través del contrato. Y lo que es particularmente agradable sobre esto es que donde hay un problema obtenemos un contra-ejemplo específico, si el contrato puede salir mal, le mostramos una manera particular en que puedes llegar a ese error, mostramos un conjunto particular de transacciones que te llevan a ese comportamiento erróneo, pero la cosa para darse cuenta aquí es que esto funciona en instancias particulares de contratos, de modo que si pensamos en el bono de cupón cero, lo rellenamos, dijimos exactamente cuál es la fecha de inicio y la fecha de finalización, dijimos exactamente cuáles son el teórico y el descuento, así que tenemos números específicos ahí, pero dado eso, es un contrato real como sería ejecutado, podemos hacer esto de forma automática y hacer pruebas exhaustivas. Ahora ¿qué tipo de cosas podemos comprobar?, supongo que la mayor propiedad crucial que podemos comprobar es si cada pago que el contrato debe hacer se ejecutará adecuadamente o hay formas de ejecutar un contrato en el que un pago puede fallar, en particular, si hay una manera en que el pago puede fallar, podemos mostrarle el camino a ese pago fallido. Así que no es sólo una cuestión de adivinar cómo podría fallar, podemos mostrar precisamente cómo puede fallar y luego puedes arreglarlo o puedes vivir con ese potencial. Otra propiedad que comprobamos es ¿hay algún pago o depósito en el contrato que va a ser por una cantidad negativa?, eso no tiene sentido, pero el contrato podría, sólo por la mecánica en la que ha sido escrito, está esa posibilidad, queremos ser capaces de comprobar que eso no pueda suceder y otras propiedades tal vez específicas de un contrato que podemos imaginar, ¿siempre resulta en que se pague más dinero a la persona 1 que a la persona 2 por ejemplo?, podríamos comprobar un número de cualquier cosa que podemos declarar sobre la forma en que los pagos toman por ejemplo, deberían ser en principio comprobable. Como esto se hace, es usando lo que se llama un solucionador SMT, SMT es una versión más sofisticada de lo que se llama un solucionador SAT, lo que en realidad es sólo una comprobación exhaustiva dónde se pueden ver que las fórmulas lógicas que se pueden hacer son satisfechas, fórmulas simples de lógica propositiva.

Pero SMT es lo que se llama teorías de módulo de satisfacción que nos permite hacer comprobación más sofisticada con aritmética y realmente lo que estamos haciendo en la comprobación de contratos Marlowe es comprobar la aritmética, usamos el solucionador SMT S3 o Z3, pero podrían utilizarse otros y tenemos una implementación en la nube para que no sea necesario instalar el solucionador por sí mismo, por supuesto, eso sería posible y obtenemos la finitud para que este solucionador funcione porque sabemos que el contrato en sí mismo es finito, sabemos que hay límites en el tamaño del estado, sabemos que hay límites en el número de transacciones, el número de entradas que podríamos tener y podemos estar seguros de que se trata de un problema finito, es solucionable. La pregunta no es si es solucionable, la pregunta es si puede ser resuelto en tiempo real y nuestra implementación inicial fue muy lenta, usamos una tecnología para traducir desde Haskell y ahora hemos reescrito eso en al menos un orden de magnitud de aceleración, así que ahora estamos recibiendo resultados nuevamente para contratos de un tamaño razonable, bastante rápido. Así que eso es completamente automático, esto puede ser pulsar un botón que te da el análisis, para saber si un contrato puede salir mal o no, así que esa es una parte del arsenal, pero como dijimos, eso es sólo para este contrato específico y estamos de acuerdo en el caso del cupón cero, hemos acordado el teórico y el descuento, hemos acordado la fecha de inicio y de finalización para que podamos hacer el análisis una vez que esas cosas se especifican, pero, ¿y si queremos probar las cosas en general?, sobre plantillas. Lo que podemos hacer entonces es usar lo que se llama verificación formal, así que esto es una prueba comprobada por máquina, así que es como escribir una prueba matemática, pero se comprueba que es correcta por el programa que hace el sistema que estamos usando, en este caso usamos el sistema llamado Isabel y lo que que Isabel nos da, la prueba está hecha como dije a mano, pero hay mucha automatización ahí, así que en muchos casos el sistema puede encontrar pruebas automáticamente. Lo que hemos hecho es que hemos sido capaces de probar propiedades de la implementación Marlowe para que podamos probar cosas sobre todo el sistema, también podríamos, en principio, no hemos llegado a esto, pero podríamos probar las propiedades de las plantillas para el contrato, para todos los calendarios de pagos posibles, independientemente del teórico y del descuento, independientemente de la fecha de inicio y de finalización, podríamos mostrar que el bono de cupón cero no produjo pagos fallidos en el caso de un garante por ejemplo. Pero en lo que me voy a concentrar aquí es en las propiedades de la plataforma y lo que hemos escrito son semánticas en Haskell, pero Isabel usa un lenguaje ligeramente diferente, si echas un vistazo a lo que tenemos aquí en Isabel y lo comparas con la implementación Haskell verás que lo que tenemos es más o menos una transliteración, una traducción línea por línea de lo que tenemos en Haskell, así que hemos sido capaces de tomar nuestra semántica, ponerla en Isabel y luego hemos sido capaces de probar las cosas. Aquí hay dos ejemplos, lo que estamos haciendo en el primer teorema aquí dice que si cada cuenta en el contrato tiene una cantidad positiva o nada en él y computamos una transacción, entonces la misma propiedad es válida de la salida de esa transacción. Así que cada transacción preservará esa propiedad, así que si empezamos, típicamente empezamos sin dinero en ninguna de las cuentas, terminamos con sólo cantidades positivas de dinero en las cuentas. Así que eso da una garantía de que la máquina se comporta independientemente de lo que ocurra, independientemente de cualquier contrato que ejecutemos. Y el segundo teorema aquí dice que una vez que hayas computado la salida de una transacción, no hay nada más que hacer hasta que otra transacción se presenta, así que el contrato es lo que llamamos quiescente después de haber computado eso. Ok, así que creo eso da algunas ilustraciones de las cosas que podemos hacer, que automáticamente podemos establecer, propiedades de contratos individuales y que, en general, podemos razonar tanto sobre las propiedades del sistema y las propiedades de las plantillas de contratos. Y estas son cosas que conseguimos porque nuestro lenguaje es un DSL, podemos hablar de todos los contratos Marlowe de una manera que no podríamos hablar de todo los programas Plutus, todos los programas de propósito general. Bien, lo que vamos a hacer ahora es echar un vistazo al Playground Marlowe que permite que pongamos todas estas cosas en práctica.