Plutus Core Team Update

High level summary

In the past weeks, the Plutus team has continued to make improvements across performance, tooling, and assurance.

Performance and compiler improvements. We improved several parts of the Plutus optimization pipeline and ledger API implementation. This includes making common Value operations more efficient, adding a new compiler optimization for certain recursive functions, and fixing an optimization pass so that it preserves program behavior correctly.

Better benchmarking and tooling. We added lightweight benchmarking support to the uplc executable, making it easier to sanity-check execution-time measurements for UPLC scripts and compare results against existing benchmark infrastructure.

Specs and formal methods. We continued strengthening the foundations of Plutus by updating the UPLC specification for the built-in value type and related functions, and by improving the metatheory and certification infrastructure used to reason about compiler transformations. These changes make the formal-assurance workflow easier to maintain, debug, and scale to larger programs.

Key Pull Requests Merged

• Specification of the built-in value type and functions
• Rename UPLC scope variable in the metatheory
• Mutually recursive PIR function inlining
• Lightweight benchmarking in the uplc executable
• Fuse unionWith and checkBinRel in PlutusLedgerApi.V1.Data.Value
• Certifier: Generate one Proof .agda file per certified pass
• Optimal non-builtin valueOf in plutus-ledger-api Data.Value
• Metatheory: define semantic versions of value and purity
• Certifier: deduplicate ASTs in agda certificate
• Fix the FloatDelay compiler optimization pass