Команда Cardano Plutus завершила модели стоимости для новых функций Dijkstra

Команда Plutus завершила модели стоимости для keepPolicies и dropPolicies, двух встроенных функций, разрабатываемых для эры Dijkstra в Cardano. В обновлении от 4 ноября руководитель направления программной инженерии Ziyang Liu также сообщил о новых тестах, обновлениях спецификаций и исправлениях компилятора.

Работа охватывает то, как смарт контракты обрабатывают значения токенов и учитывают ресурсы исполнения. Это изменения на этапе разработки, поддерживающие подготовку к Dijkstra, при этом в отчете не объявляется их активация в основной сети Cardano.

Новые функции фильтруют токены по политикам

Эти две функции входят в CIP-0168, предложение, расширяющее операции над BuiltinValue, типом данных, используемым для представления количеств активов в смарт контрактах Plutus. Встроенные функции предоставляют операции, напрямую поддерживаемые системой исполнения.

Cardano группирует нативные токены по идентификаторам политик, связанным с их правилами выпуска. keepPolicies сохраняет части значения, связанные с выбранными идентификаторами, тогда как dropPolicies удаляет их. Контракт, обрабатывающий несколько групп токенов, может использовать эти функции, чтобы изолировать активы, относящиеся к конкретной проверке.

Объединенные изменения ограничивают список политик, принимаемый любой из функций, 256 идентификаторами. Завершенные модели стоимости определяют, как исполнение учитывается в единицах CPU и памяти, которые входят в бюджет исполнения смарт контракта.

Тесты и исправления компилятора затрагивают поведение программ

Команда добавила 65 тестов на соответствие для новых встроенных функций Value. Эти тесты сравнивают вывод реализации с ожидаемым результатом для заданных входных данных. Новые функции и multiIndexArray также задокументированы в спецификации Plutus Core, предоставляя письменное описание их поведения.

Отдельное исправление касается constant folding, оптимизации, которая вычисляет подходящие выражения во время компиляции вместо того, чтобы оставлять их на исполнение. Затронутые проходы компилятора ранее могли упрощать некоторые выражения способом, который неправильно отбрасывал вычисления, которые завершаются с ошибкой. Исправление сохраняет такие вычисления, когда необходимые условия для упрощения не выполнены.

Обновление также исправляет компиляцию типов контекста Plutus V4, которые описывают информацию, доступную сценариям при проверке транзакций. Кроме того, модели памяти для lookupCoin и valueContains приведены в соответствие с имеющимися параметрами модели стоимости.

[NEWSBREAK]

Формальные проверки расширяются по мере продолжения реализации

Команда представила инструмент, который генерирует тесты на проверку типов в Agda из существующего набора тестов на соответствие. Agda это язык программирования и ассистент доказательств, используемый для выражения формальных моделей и проверки их согласованности. Инструмент позволяет уже используемым для реализации тестовым случаям поддерживать проверки в этой формальной среде.

Новые встроенные функции также добавлены в метатеорию, математическое описание, используемое для рассуждений о программах Plutus. В настоящее время они представлены как постулаты, что означает, что модель предполагает их заданное поведение, пока работа над дальнейшей реализацией продолжается. Другое объединенное изменение расширяет инструмент, который проверяет, сохраняет ли оптимизация компилятора поведение программы.

Оставшаяся работа включает внедрение массивов и байтовых строк в формальную модель, исправление сертификации отдельной оптимизации компилятора и улучшение машины CEK, которая исполняет программы Plutus Core. Эти пункты по прежнему числятся как находящиеся в работе в отчете от 4 ноября.