Skip to content

Commit f96014f

Browse files
committed
test(cek): add boundary and VConstr discharge tests
Add shift==idx boundary test verifying bound variable detection, and VConstr test verifying free variables in constructor arguments are shifted correctly under lambdas.
1 parent 6b5e5ce commit f96014f

1 file changed

Lines changed: 32 additions & 0 deletions

File tree

  • plutus-core/untyped-plutus-core/testlib/Evaluation

plutus-core/untyped-plutus-core/testlib/Evaluation/FreeVars.hs

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,10 @@ testDischargeFree =
7777
, ("freeVarPastNonEmptyEnvWithLambda", freeVarPastNonEmptyEnvWithLambda)
7878
, ("freeVarPastNonEmptyEnvNested", freeVarPastNonEmptyEnvNested)
7979
, ("freeVarMixedBoundAndTrulyFree", freeVarMixedBoundAndTrulyFree)
80+
, -- Edge case: shift == idx boundary (variable bound by the immediately enclosing lambda)
81+
("boundaryShiftEqualsIdx", boundaryShiftEqualsIdx)
82+
, -- Constructor arguments containing free variables
83+
("constrWithFreeVars", constrWithFreeVars)
8084
]
8185
where
8286
delayWithEmptyEnv =
@@ -290,6 +294,34 @@ testDischargeFree =
290294
-- x stays, unit substituted, free var 3 → var 4
291295
)
292296

297+
boundaryShiftEqualsIdx =
298+
-- VLamAbs _ (var 1) []
299+
-- Under 1 lambda (shift=1), var 1 with idx=1: shift >= idx is true, so bound.
300+
-- This tests the exact boundary of the bound-vs-free check.
301+
dis
302+
( VLamAbs
303+
(fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
304+
(toFakeTerm $ v 1)
305+
[]
306+
)
307+
@?= DischargeNonConstant (toFakeTerm . lamAbs0 $ v 1)
308+
309+
constrWithFreeVars =
310+
-- VConstr 0 [VDelay (var 1) []] discharged under 1 lambda from outer env
311+
-- The VDelay contains a free var; when discharged under the outer lambda
312+
-- the free var should be shifted.
313+
dis
314+
( VLamAbs
315+
(fakeNameDeBruijn $ DeBruijn deBruijnInitIndex)
316+
(toFakeTerm $ v 2)
317+
[ VConstr 0 (MultiStack (LastStackNonEmpty (VDelay (toFakeTerm $ v 1) [])))
318+
]
319+
)
320+
@?= DischargeNonConstant
321+
( toFakeTerm . lamAbs0 $
322+
Constr () 0 [Delay () (v 2)] -- var 1 shifted by 1
323+
)
324+
293325
dis = dischargeCekValue @DefaultUni @DefaultFun
294326
v = Var () . DeBruijn
295327

0 commit comments

Comments
 (0)