El equipo de Plutus de Cardano finaliza los modelos de costos para las nuevas funciones de Dijkstra

El equipo de Plutus ha finalizado los modelos de costos para keepPolicies y dropPolicies, dos funciones integradas que se están desarrollando para la era Dijkstra de Cardano. En una actualización del 4 de noviembre, el líder de ingeniería de software Ziyang Liu también informó sobre nuevas pruebas, actualizaciones de especificaciones y correcciones del compilador.

El trabajo abarca cómo los contratos inteligentes gestionan los valores de tokens y contabilizan los recursos de ejecución. Se trata de cambios de desarrollo que respaldan la preparación de Dijkstra; el informe no anuncia su activación en la red principal de Cardano.

Nuevas funciones filtran tokens por política

Ambas funciones pertenecen a CIP-0168, una propuesta que amplía las operaciones sobre BuiltinValue, el tipo de datos utilizado para representar cantidades de activos dentro de los contratos inteligentes de Plutus. Las funciones integradas proporcionan operaciones admitidas directamente por el sistema de ejecución.

Cardano agrupa los tokens nativos bajo identificadores de política asociados con sus reglas de acuñación. keepPolicies conserva las porciones de un valor asociadas con identificadores seleccionados, mientras que dropPolicies las elimina. Un contrato que procese varios grupos de tokens podría usar estas funciones para aislar los activos relevantes para una verificación determinada.

Los cambios fusionados limitan a 256 identificadores la lista de políticas aceptada por cualquiera de las dos funciones. Sus modelos de costos completados definen cómo se contabiliza la ejecución en unidades de CPU y memoria, que forman parte del presupuesto de ejecución de un contrato inteligente.

Las pruebas y correcciones del compilador abordan el comportamiento de los programas

El equipo añadió 65 casos de conformidad para las nuevas funciones integradas de Value. Estas pruebas comparan la salida de la implementación con el resultado esperado para entradas definidas. Las nuevas funciones y multiIndexArray también se han documentado en la especificación de Plutus Core, proporcionando una referencia escrita de su comportamiento.

Una corrección aparte aborda el constant folding, una optimización que calcula expresiones adecuadas durante la compilación en lugar de dejarlas para la ejecución. Las fases del compilador afectadas podían simplificar anteriormente ciertas expresiones de una manera que descartaba incorrectamente las computaciones que fallan. La corrección preserva esas computaciones cuando no se cumplen las condiciones necesarias para la simplificación.

La actualización también corrige la compilación de los tipos de contexto de Plutus V4, que describen la información disponible para los scripts al validar transacciones. Además, los modelos de memoria para lookupCoin y valueContains se han alineado con los parámetros existentes del modelo de costos.

[NEWSBREAK]

Las comprobaciones formales se amplían a medida que continúa la implementación

El equipo presentó una herramienta que genera pruebas de comprobación de tipos en Agda a partir del conjunto de conformidad existente. Agda es un lenguaje de programación y asistente de pruebas usado para expresar modelos formales y verificar su consistencia. La herramienta permite que los casos de prueba ya usados para la implementación respalden comprobaciones en ese entorno formal.

Las nuevas funciones integradas también se han añadido a la metateoría, la descripción matemática utilizada para razonar sobre programas de Plutus. Actualmente aparecen como postulados, lo que significa que el modelo asume su comportamiento especificado mientras continúa el trabajo de implementación. Otro cambio fusionado amplía una herramienta que verifica si una optimización del compilador preserva el comportamiento del programa.

El trabajo pendiente incluye implementar arreglos y cadenas de bytes en el modelo formal, corregir la certificación de una optimización distinta del compilador y mejorar la máquina CEK que ejecuta programas de Plutus Core. Estos elementos siguen listados como trabajo en curso en el informe del 4 de noviembre.