Il team Plutus di Cardano finalizza i modelli di costo per le nuove funzioni di Dijkstra

Il team Plutus ha finalizzato i modelli di costo per keepPolicies e dropPolicies, due funzioni integrate in fase di sviluppo per l’era Dijkstra di Cardano. In un aggiornamento del 4 novembre, il responsabile dell’ingegneria software Ziyang Liu ha inoltre segnalato nuovi test, aggiornamenti alle specifiche e correzioni al compilatore.

Il lavoro riguarda il modo in cui gli smart contract gestiscono i valori dei token e contabilizzano le risorse di esecuzione. Si tratta di modifiche di sviluppo a supporto della preparazione di Dijkstra; il rapporto non annuncia la loro attivazione sulla mainnet di Cardano.

Nuove funzioni filtrano i token per policy

Le due funzioni appartengono a CIP-0168, una proposta che estende le operazioni su BuiltinValue, il tipo di dato utilizzato per rappresentare le quantità di asset all’interno degli smart contract Plutus. Le funzioni integrate forniscono operazioni supportate direttamente dal sistema di esecuzione.

Cardano raggruppa i token nativi sotto identificatori di policy associati alle loro regole di conio. keepPolicies conserva le porzioni di un valore associate agli identificatori selezionati, mentre dropPolicies le rimuove. Un contratto che elabora diversi gruppi di token potrebbe usare queste funzioni per isolare gli asset pertinenti a un determinato controllo.

Le modifiche unite limitano a 256 identificatori l’elenco di policy accettato da ciascuna funzione. I relativi modelli di costo definitivi specificano come l’esecuzione venga contabilizzata in unità di CPU e memoria, che costituiscono parte del budget di esecuzione di uno smart contract.

Test e correzioni del compilatore affrontano il comportamento dei programmi

Il team ha aggiunto 65 casi di conformità per i nuovi builtins di Value. Questi test confrontano l’output dell’implementazione con il risultato atteso per input definiti. Le nuove funzioni e multiIndexArray sono state inoltre documentate nella specifica di Plutus Core, fornendo un riferimento scritto per il loro comportamento.

Un’altra correzione riguarda il constant folding, un’ottimizzazione che calcola alcune espressioni durante la compilazione invece di lasciarle all’esecuzione. I passaggi del compilatore interessati potevano in precedenza semplificare certe espressioni in modo da scartare erroneamente le computazioni che falliscono. La correzione preserva tali computazioni quando non sono soddisfatte le condizioni necessarie per la semplificazione.

L’aggiornamento corregge anche la compilazione dei tipi di contesto di Plutus V4, che descrivono le informazioni disponibili agli script durante la validazione delle transazioni. Inoltre, i modelli di memoria per lookupCoin e valueContains sono stati allineati ai parametri del modello di costo esistente.

[NEWSBREAK]

I controlli formali si espandono mentre prosegue l’implementazione

Il team ha introdotto uno strumento che genera test di typechecking in Agda a partire dalla suite di conformità esistente. Agda è un linguaggio di programmazione e un assistente alla dimostrazione utilizzato per esprimere modelli formali e verificarne la coerenza. Lo strumento consente ai casi di test già usati per l’implementazione di supportare verifiche in quell’ambiente formale.

I nuovi builtins sono stati aggiunti anche alla metateoria, la descrizione matematica usata per ragionare sui programmi Plutus. Attualmente appaiono come postulati, il che significa che il modello assume il loro comportamento specificato mentre prosegue il lavoro di implementazione. Un’altra modifica unita estende uno strumento che verifica se un’ottimizzazione del compilatore preserva il comportamento del programma.

Il lavoro rimanente include l’implementazione di array e byte string nel modello formale, la correzione della certificazione di un’ottimizzazione separata del compilatore e il miglioramento della macchina CEK che esegue i programmi Plutus Core. Questi elementi restano elencati come lavori in corso nel rapporto del 4 novembre.