Cardano Plutus チームが Dijkstra の新関数のコストモデルを最終確定

Plutus チームは、Cardano の Dijkstra 期向けに開発中の二つの組み込み関数 keepPolicies と dropPolicies のコストモデルを最終確定した。11月4日のアップデートで、Software Engineering Lead の Ziyang Liu は新たなテスト、仕様の更新、コンパイラの修正についても報告した。

今回の作業は、スマートコントラクトがトークンの値をどのように扱い、実行リソースをどのように計上するかを対象としている。これらは Dijkstra の準備を支える開発上の変更であり、レポートは Cardano メインネットでの有効化を発表してはいない。

新しい関数はポリシーでトークンをフィルタリング

これら二つの関数は CIP-0168 に属し、Plutus のスマートコントラクト内で資産数量を表すデータ型 BuiltinValue に対する操作を拡張する提案である。組み込み関数は、実行システムが直接サポートする操作を提供する。

Cardano では、ネイティブトークンは鋳造ルールに関連付けられたポリシー識別子の下にグループ化される。keepPolicies は選択した識別子に関連する値の部分を保持し、dropPolicies はそれらを除去する。複数のトークングループを処理するコントラクトは、特定の検証に関係する資産だけを切り出すためにこれらの関数を利用できる。

マージされた変更により、両関数が受け付けるポリシーリストは最大256個の識別子に制限された。完成したコストモデルは、CPU とメモリの単位で実行をどのように計上するかを定義しており、これはスマートコントラクトの実行予算の一部を構成する。

テストとコンパイラ修正はプログラムの挙動に対応

チームは新しい Value の組み込み関数に対して65件の適合性テストケースを追加した。これらのテストは、定義された入力に対する実装の出力を期待される結果と比較するものだ。新しい関数および multiIndexArray も Plutus Core 仕様に文書化され、その挙動に関する参照が提供された。

別の修正はコンスタントフォールディングに関するものだ。これは、実行時ではなくコンパイル時に適切な式を計算する最適化である。影響を受けたコンパイラのパスは、以前は特定の式を単純化する際に、失敗すべき計算を誤って捨ててしまう可能性があった。今回の修正により、単純化の要件が満たされない場合はそれらの計算が保持される。

このアップデートでは、トランザクション検証時にスクリプトが利用可能な情報を記述する Plutus V4 のコンテキスト型のコンパイルも修正された。加えて、lookupCoin と valueContains のメモリモデルが既存のコストモデルのパラメータに合わせて調整された。

[NEWSBREAK]

実装の進展に伴い形式的な検証が拡大

チームは、既存の適合性スイートから Agda での型検査テストを生成するツールを導入した。Agda は、形式モデルを表現しその整合性を検証するために用いられるプログラミング言語兼証明支援系である。このツールにより、実装で既に用いられているテストケースを、その形式的な環境での検証にも活用できる。

新しい組み込み関数は、Plutus プログラムについて推論するための数学的記述であるメタ理論にも追加された。現在は公理として現れており、さらなる実装作業が進む間は、その仕様どおりの挙動をモデルが仮定することを意味する。さらに、コンパイラ最適化がプログラムの挙動を保持しているかを検査するツールを拡張する変更もマージされた。

残る作業には、形式モデルにおける配列とバイト文字列の実装、別のコンパイラ最適化の検証の是正、Plutus Core プログラムを実行する CEK マシンの改良が含まれる。これらの項目は、11月4日のレポートで進行中の作業として引き続き記載されている。