L’équipe Plutus de Cardano finalise les modèles de coûts pour les nouvelles fonctions de Dijkstra

L’équipe Plutus a finalisé les modèles de coûts pour keepPolicies et dropPolicies, deux fonctions intégrées en cours de développement pour l’ère Dijkstra de Cardano. Dans une mise à jour du 4 novembre, le responsable de l’ingénierie logicielle Ziyang Liu a également annoncé de nouveaux tests, des mises à jour de spécifications et des correctifs du compilateur.

Les travaux portent sur la manière dont les contrats intelligents gèrent les valeurs de jetons et tiennent compte des ressources d’exécution. Il s’agit de changements de développement destinés à préparer Dijkstra, le rapport n’annonce pas leur activation sur le mainnet Cardano.

De nouvelles fonctions filtrent les jetons par politique

Les deux fonctions relèvent de CIP-0168, une proposition qui étend les opérations sur BuiltinValue, le type de données utilisé pour représenter les quantités d’actifs dans les contrats intelligents Plutus. Les fonctions intégrées fournissent des opérations directement prises en charge par le système d’exécution.

Cardano regroupe les jetons natifs sous des identifiants de politique associés à leurs règles de frappe. keepPolicies conserve les portions d’une valeur associées aux identifiants sélectionnés, tandis que dropPolicies les supprime. Un contrat traitant plusieurs groupes de jetons pourrait utiliser ces fonctions pour isoler les actifs pertinents pour une vérification particulière.

Les changements fusionnés limitent la liste d’identifiants de politique acceptée par chaque fonction à 256 identifiants. Leurs modèles de coûts finalisés définissent la manière dont l’exécution est comptabilisée en unités CPU et mémoire, qui font partie du budget d’exécution d’un contrat intelligent.

Des tests et des correctifs du compilateur traitent le comportement des programmes

L’équipe a ajouté 65 cas de conformité pour les nouveaux builtins de Value. Ces tests comparent la sortie de l’implémentation au résultat attendu pour des entrées définies. Les nouvelles fonctions et multiIndexArray ont également été documentées dans la spécification de Plutus Core, offrant une référence écrite pour leur comportement.

Une correction distincte concerne le constant folding, une optimisation qui calcule certaines expressions à la compilation au lieu de les laisser pour l’exécution. Les passes du compilateur concernées pouvaient auparavant simplifier certaines expressions d’une manière qui écartait à tort des calculs qui échouent. Le correctif préserve ces calculs lorsque les conditions requises pour la simplification ne sont pas remplies.

La mise à jour corrige aussi la compilation des types de contexte de Plutus V4, qui décrivent les informations disponibles pour les scripts lors de la validation des transactions. En outre, les modèles mémoire pour lookupCoin et valueContains ont été alignés sur les paramètres existants du modèle de coûts.

[NEWSBREAK]

Les vérifications formelles s’étendent à mesure que l’implémentation progresse

L’équipe a introduit un outil qui génère des tests de vérification de types dans Agda à partir de la suite de conformité existante. Agda est un langage de programmation et un assistant de preuve utilisé pour exprimer des modèles formels et vérifier leur cohérence. L’outil permet aux cas de test déjà utilisés pour l’implémentation de servir aux vérifications dans cet environnement formel.

Les nouveaux builtins ont aussi été ajoutés à la métathéorie, la description mathématique utilisée pour raisonner sur les programmes Plutus. Ils apparaissent actuellement comme des postulats, ce qui signifie que le modèle suppose leur comportement spécifié tandis que les travaux d’implémentation se poursuivent. Un autre changement fusionné étend un outil qui vérifie si une optimisation du compilateur préserve le comportement des programmes.

Le travail restant comprend l’implémentation des tableaux et des chaînes d’octets dans le modèle formel, la correction de la certification d’une optimisation distincte du compilateur, et l’amélioration de la machine CEK qui exécute les programmes Plutus Core. Ces éléments restent listés comme en cours dans le rapport du 4 novembre.