input-output-hk / input-output-hk/PlutusCoreBlaster

[Bug]: BLS12-381 conformance tests fail budget checks by ~70-105x due to a stale, never-regenerated test suite

Open
#35 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
Lean
Stars
14
Forks
6
Avg merge
4d 8h
Merged PRs (30d)
2

Description

## Description

Running the official `plutus-conformance` BLS12-381 test cases against this Lean formalization, the majority fail their budget check by very large, non-uniform margins (roughly 1.1x to 235x depending on the specific test). For example, `bls12_381_G1_add`'s `add`/`add-zero` cases compute `cpu=109,815,357` where `Tests/Conformance/Generated/Builtin/Semantics/Bls12_381_G1_add/Add.lean` hardcodes an expected value of `cpu=1,042,435` (~105x).

This is **not a CEK machine or cost-model bug**. `Tests/Conformance/Generated/` was generated once, on 2026-05-18, and has never been regenerated since. Two upstream `plutus` changes made it stale:

1. `IntersectMBO/plutus#7837` ("Refactor BLS12_381 conformance tests to remove literal curve points", 2026-07-10) rewrote the BLS12-381 test *programs* themselves to derive curve points via `bls12_381_G1/G2_uncompress` calls on raw bytestrings instead of embedding pre-decoded `bls12_381_G1_element`/`G2_element` constants directly (and wrap results in `compress` where the original returned a point). This is genuinely more builtin work per test program, so the correct expected budget grew accordingly — it is not a cost-model recalibration. This also explains the non-uniform ratios: each test's increase tracks how many curve-point arguments it has (i.e. how many extra `uncompress`/`compress` calls the refactor added), not a single scaling factor.
2. The `builtin/constant/` test category (including `builtin/constant/bls12-381/G1|G2/*`) was removed upstream entirely, superseded by a new `builtin/parser/` category covering the same cases.

Live-evaluating several of the "failing" cases directly through `cekExecuteProgramWithBudget` (spanning `bls12_381_G1_add`, `bls12_381_G2_multiScalarMul`, and `bls12_381_millerLoop`) matches the *current* `.budget.expected` files in `plutus-conformance` exactly, including memory. Lean's BLS12-381 cost formulas are correct against the current cost model.

Regenerating `Tests/Conformance/Generated/` against a current `plutus` checkout also surfaces two small, unrelated compatibility bugs in `scripts/GenConformanceTests.lean` that block the regeneration itself:

- Expected-budget files dropped their `.uplc` infix upstream (`{stem}.uplc.budget.expected` → `{stem}.budget.expected}`), which the generator doesn't account for.
- The parse-error marker text changed from `"parse error"` to `"parse/decode error"`, which the generator doesn't recognize.

## Steps to Reproduce

```
lake exe gen_conformance_tests .plutus-conformance/plutus-conformance \
--out Tests/Conformance/Generated \
--embed-root .plutus-conformance/plutus-conformance \
--exclude-not-implemented
```
against a current `IntersectMBO/plutus` checkout: fails with `uncaught exception: failed to classify .../builtin/interleaving/ite: could not parse budget file` (naming-convention bug), and again later at `builtin/parser/array/illTypedArray-01` once that's fixed (wording bug).

Absent those, `lake build Tests.Conformance.Generated` against the *currently committed* (stale) suite: 119 of 185 BLS12-381-related budget checks fail.

## Expected Behavior

`Tests/Conformance/Generated/` should reflect a current `plutus-conformance` checkout, and `scripts/GenConformanceTests.lean` should be able to regenerate it without manual patching.

## Actual Behavior

The generated suite is stale (last generated 2026-05-18) and the generator script itself has two small compatibility gaps that block regenerating it against the current corpus.

## Lean Version

v4.24.0

## Z3 Version

N/A (no SMT tactics involved)

Contributor guide

No contributing guide indexed for this repository

Research direction

Start with scripts/GenConformanceTests.lean and reproduce the lake exe gen_conformance_tests command against the current plutus-conformance checkout. Update the generator for the current budget filename convention and parse-error marker, regenerate Tests/Conformance/Generated, then run lake build Tests.Conformance.Generated and verify the BLS12-381 budget checks pass.

Written by the indexing model from the issue text.

Assessment

Domain
build-system, testing
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Quiet
Clarity
Clearly specified
Newbie friendliness
55/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.