Plutus Core Team Update

High level summary

The Plutus team has continued work on the Dijkstra builtins and conformance testing. In particular we've finalized the cost models of the keepPolicies and dropPolicies builtins (CIP-0168). We've also added 65 conformance cases for the new Value builtins, and specified these builtins and multiIndexArray in the Plutus Core specification.

On the metatheory front, a new tool generates Agda typechecking tests from the conformance suite. We've also added the new builtins to the metatheory as postulates, and added support for casing on Data to the certifier's case-reduce pass.

Other than these, we've fixed the PIR and UPLC constant folding passes so they no longer fold builtin applications with impure arguments, which could incorrectly discard computations that fail. We've also fixed compilation of Plutus V4 context types and aligned the lookupCoin and valueContains memory models with the existing cost-model parameters.

Work in progress includes implementing arrays and bytestrings in the metatheory, fixing certification of the case-of-case pass, and further CEK machine optimizations.

Key Pull Requests Merged

• Limit the policy list of keepPolicies and dropPolicies to 256 ids
• Conformance tests for CIP-0168 Value builtins
• Specify batch 7 builtins
• Add tool to generate Agda typechecking tests from conformance tests
• Add batch 7 builtins to the metatheory and Data casing to the case-reduce certifier
• Fix PIR's and UPLC's constant folding passes
• Expose all unfoldings for PlutusLedgerApi.V4.Contexts
• Fix lookupCoin and valueContains memory models to match the committed JSON
• Deploy to gh-pages without checking out the whole branch

Pull Requests In Progress

• Metatheory: implement BuiltinArray
• Add bytestring to metatheory
• Certifier: case-of-case pass
• Replace Vector with Array in the evaluator