PlutusCore | Reservoir

PlutusCoreBlaster

PlutusCoreBlaster is a Lean 4 formalization of Untyped Plutus Core (UPLC), the smart contract execution language of Cardano. It provides UPLC syntax, decoders, a CEK evaluator, builtin functions, tests, and tools for preparing programs for proofs. The project is working toward conformance with the Haskell reference implementation; see Conformance testing for the current scope.

Installation and building

Install z3 version 4.15.2. Install Lean 4 through elan. The version selected by this repository is recorded in lean-toolchain (currently 4.24.0). Lake fetches the Lean-blaster dependency; the Cryptograph library is included in this repository.

lake build          # build the default PlutusCore target
lake build Lemmas   # build the proof library
lake test           # build the standard test suite

The corresponding Make targets are make build_plutus_core, make build_tests, and make check_all. The check_* targets also check that the expected Lean files are covered by their builds.

Using the library

The Lake package is named PlutusCore, while the Git repository is named PlutusCoreBlaster. Add it to your project's Lake configuration in either format:

# lakefile.toml
[[require]]
name = "PlutusCore"
git = "https://github.com/input-output-hk/PlutusCoreBlaster"
rev = "main"

-- lakefile.lean
require «PlutusCore» from git
  "https://github.com/input-output-hk/PlutusCoreBlaster" @ "main"

For reproducible builds, replace main with a commit or release tag that you have tested.

Libraries and modules

Library or module	Purpose
`PlutusCore.UPLC.Term`	UPLC terms, programs, constants, and builtin names
`PlutusCore.UPLC.CekMachine`	CEK evaluation with a step limit or an execution budget
`PlutusCore.UPLC.BuiltinFunctions`	Arithmetic, byte strings, cryptography, data, lists, pairs, and bitwise operations
`PlutusCore.UPLC.TextEncoding`	Parser for textual `.uplc` programs
`PlutusCore.UPLC.FlatEncoding`	Decoder for Flat-encoded programs
`PlutusCore.UPLC.ScriptEncoding`	Decoders and import commands for Flat, CBOR-wrapped, hexadecimal, and textual scripts
`PlutusCore.UPLC.PlutusScript`	Script envelope and Plutus V1/V2/V3 language tags
`PlutusCore.UPLC.PreProcess`	`#prep_uplc` command for preparing proof and execution expressions
`Cryptograph`	Bundled BLS12-381, Ed25519, Secp256k1, hash, and modular arithmetic code
`Lemmas`	Proofs and helper lemmas for the formalization

The CEK machine has four states: Eval, Return, Error, and Halt. Its step-limited execution and budget-aware execution use the same UPLC model. Some newer array and value/coin features are not implemented yet; see Current scope.

Preparing a UPLC program

#prep_uplc takes a named PlutusScript, an optional input-conversion function, and a maximum number of CEK steps. It creates a named structure with lang, prop (the optimized expression for proofs), and exec (the original expression for execution). For example, this closed program is adapted from PlutusCore/UPLC/PreProcess/Tests.lean:

import PlutusCore.UPLC.PreProcess

open PlutusCore.UPLC.PlutusScript (PlutusScript)
open PlutusCore.UPLC.Term (Program Version Term Const)

def answerScript : PlutusScript :=
  { lang := .PlutusV3
    script := Program.Program (Version.Version 1 1 0)
      (Term.Const (Const.Integer 42)) }

#prep_uplc preparedAnswer answerScript 10
#check preparedAnswer.prop
#check preparedAnswer.exec

The final number is a step limit, not a CPU or memory ExBudget. Programs that take inputs can provide an input-conversion function before that number; see the syntax and example in PreProcess.lean.

Testing

lake test
# or: make build_tests

The standard Tests target covers encoding and CBOR, bitwise operations, CEK execution, preprocessing, cryptographic vectors, and equality. It includes textual UPLC parser tests. It does not run the generated conformance suite.

Conformance testing

The generator in scripts/GenConformanceTests.lean derives Lean cases from the Plutus conformance corpus. The generated tests compare evaluation results and execution budgets with the reference expectations. Categories that rely on features not yet implemented can be excluded during generation (including array and value/coin operations).

The conformance suite needs the external Plutus corpus at .plutus-conformance/plutus-conformance. After providing that path, run:

make gen_conformance_tests excludeNotImplemented=1
make check_conformance

The conformance workflow runs separately from the normal CI. A maintainer can trigger it on a PR with /run-conformance or run it manually. A passing lake test does not imply that all conformance cases pass.

Benchmarks

The #prep_uplc benchmark suite measures preprocessing time and memory and can compare two runs. See Benchmark/README.md for requirements, case selection, commands, and result fields.

make build_benchmark
make bench_prep_uplc BENCH_ARGS="--suite repo,symbolic"

Current scope

Component	State
UPLC syntax and CEK evaluation	Implemented; the budgeted evaluator's termination proof is pending
Text, Flat, and script decoding	Implemented for supported UPLC features
Builtin functions and cryptographic primitives	Implemented for supported batches; array and value/coin features remain open
Standard tests	Built by `lake test`
Formal proofs in `Lemmas`	In progress
Reference conformance	Generated and checked separately; unsupported categories can be excluded

Contributing

Bug reports, documentation improvements, tests, and code changes are welcome. Open an issue to discuss a problem or submit a pull request. Before submitting code, run make check_all; changes affecting reference behavior may also need a conformance run.

Maintainers: Jean-Frédéric Etienne, Romain Soulat, and Mark Petruska.