Plutus Core Team Update

High level summary

Plutus Core

• We merged the PR adding support for case analysis on booleans and integers. Our current focus is extending this support to built-in lists.

• Several improvements have also been made to the Plutus Core specification.

• A new tool was merged and released to dump cost model parameters in the format expected by the node. It supports multiple output formats and can be particularly useful when adding new primitives or updating cost model parameters for other reasons.

Plinth

• We implemented and merged a compiler optimization that pushes force nodes into case branches. This often enables subsequent optimizations by eliminating adjacent force and delay pairs.

• To benchmark the Plinth compiler and identify further optimization opportunities, we reimplemented in plutus-benchmarks the linear vesting script (originally written in Plutarch) in Plinth.

Formal Methods

• We are now releasing plutus-metatheory on CHaP, which is a prerequisite for releasing the compiler certifier alongside the Plinth compiler.

Low level summary

Key Pull Requests Merged

• Case analysis on booleans and integers
• Add plutus-metatheory to CHaP release process
• spec: Make case and constr indexes start from 1
• Correct the specification of the flat encoding of constr tags
• Implement force-case-delay optimisation
• Extra Modular Exponentiation property tests
• Add Linear Vesting script to the benchmark
• Tool to dump cost model parameters in order expected by ledger

Issues and Pull Requests In Progress

• Case analysis on built-in lists
• Push 'force' into 'chooseList' and 'chooseData'
• Call trace for failing evaluation via new emitter mode
• Add builtin arrays to Plutus metatheory
• Add MSM builtin