IntersectMBO/plutus

`dischargeCekValue` doesn't handle open terms correctly

Open

#7526 opened on Jan 15, 2026

View on GitHub
 (5 comments) (1 reaction) (1 assignee)Haskell (1,637 stars) (511 forks)batch import
Good first issuebugstatus: triaged

Description

dischargeCekValue has the following code:

                  -- var is free, leave it alone
                  (Var () named)

which means that

(\0 \0 var 2) (delay (var 1))

evaluates to

[1 :-> delay (var 1)] (\0 var 2)

which then discharges to

\0 delay (var 1)

which is variable capture.

Contributor guide

Tech stack
None
Domain
backend
Issue type
bug
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
4
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-3 hours
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
blocked
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
clear
Prerequisites
basic Haskelllambda calculus
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
25
Research direction
The bug is in the `dischargeCekValue` function within the Plutus codebase. Start by locating this function, likely in a file related to the CEK machine evaluator. The issue describes variable capture when handling free variables. Review the specific case for `Var () named` and understand how the substitution is performed. Check if there are any existing tests for this behavior. The current assignee may have additional context; consider reviewing any comments for further guidance.