Análisis estático

Una característica distintiva de Marlowe -probablemente la más distintiva- es que podemos analizar los contratos, y deducir sus propiedades, sin ejecutarlos.

Podemos comprobar, antes de ejecutar un contrato, estas propiedades:

Pagos parciales: es decir, pagos cuando no había suficiente dinero en la cuenta.
Depósitos no positivos: en los que el contrato pide un valor negativo o cero.
Pagos no positivos: pagos de 0 o un importe negativo.
Sombreado de Lets , donde dos Lets fijan el mismo identificador en la misma ruta de ejecución.

En el resto de este tutorial nos centraremos en el primero de ellos, que es el peor tipo de error. Es en este caso que un pago falla, porque no hay suficiente dinero en el contrato (o más estrictamente en la cuenta) para hacer un pago completo.

Un ejemplo

Veamos este ejemplo, en Blockly

Y en puro Marlowe

El contrato exige en primer lugar un depósito de Alice de 1 Lovelace, y luego le pide a Bob que haga una elección (llamada bool) de 0 o 1. El contrato paga entonces esta elección más uno a Bob con cargo a la cuenta de Alice.

Así, podemos ver que mientras el contrato funciona bien cuando Bob elige 0, no habrá suficiente en el contrato para pagarle si elige 1. Nuestro análisis, que está integrado en la pestaña SIMULATION del Marlowe Playground, puede diagnosticar esto:

Esto muestra que el error se produce cuando

Alice ha hecho el depósito, y
Bob ha elegido el valor 1.

y que el error generado es un TransactionPartialPay: en este caso Bob sólo recibe un pago de 1 en lugar de 2.

Si modificamos el contrato para que Alice haga un depósito inicial de 2, entonces el análisis tendrá éxito:

Bajo el capó

Sólo para reiterar: el efecto de este análisis es comprobar cada posible ruta de ejecución a través del contrato, utilizando una versión simbólica del mismo. Esto se pasa al solucionador Z3 SMT, que es un sistema automatizado de última generación para decidir si las fórmulas lógicas son satisfechas.

Si el análisis no tiene éxito, es decir, si hay una forma de hacer que el contrato falle un pago, entonces el sistema también dará un ejemplo de cómo puede salir mal, y lo presentará al usuario. El usuario puede entonces arreglar el problema y volver a comprobarlo.

Próximos pasos

En los próximos meses estudiaremos cómo presentar los resultados de nuestro análisis de una manera más "amigable", así como ampliar el alcance de nuestro trabajo.

Utiliza el botón de análisis en el Marlowe Playground para analizar algunos de los contratos que ya has escrito. Si el análisis falla, ¿puedes ver por qué y corregir los contratos para que no fallen?

Encuentra una copia oficial de este documento aquí:

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

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

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