#prep_uplc scales poorly on large UPLC validators during CEK runSteps/step reduction

## Summary

`#prep_uplc` can become prohibitively expensive when preparing larger imported UPLC validators. The hot path appears to be Blaster optimization of symbolic CEK execution, especially match reduction / WHNF around `runSteps`, `step`, and builtin evaluation.

Related issues:

- https://github.com/input-output-hk/Lean-blaster/issues/123
- https://github.com/input-output-hk/Lean-blaster/issues/72
- https://github.com/input-output-hk/Lean-blaster/issues/63
- https://github.com/input-output-hk/Lean-blaster/issues/52
- https://github.com/input-output-hk/Lean-blaster/issues/119

## Observed behavior

For a nonrecursive Plutus V3 validator imported through `#import_uplc`, `#prep_uplc` spends most of its time optimizing the specialized CEK interpreter state, before theorem solving.

Instrumentation pointed at:

- `PlutusCore.UPLC.CekMachine.runSteps.match_1`
- `PlutusCore.UPLC.CekMachine.step.match_3`
- `PlutusCore.UPLC.CekMachine.ifBoundOtherwiseError.match_1`
- `PlutusCore.UPLC.CekMachine.evalBuiltin.match_1`
- `PlutusCore.UPLC.BuiltinFunctions.Evaluate.evaluateBuiltinFunction.match_1`

Representative active CEK states involved builtin/data evaluation around `IfThenElse`, `UnMapData`, `UnConstrData`, `SndPair`, `HeadList`, `NullList`, `LessThanInteger`, and `EqualsData`.

## Measurements

Using a local instrumented build:

- 51 fuel, checkpoint chunk 50: `Prepared` built in 5.5s
- 501 fuel, checkpoint chunk 50: `Prepared` built in 171s
- 15,598,844 optimizer stack steps
- 217,453 `reduceMatch` calls
- 154,261 `reduceMatch` hits
- 92,732 `reduceApp` hits
- 10,000 fuel, checkpoint chunk 50: still CPU-bound in Lean when killed after 627.719s
- 10,000 fuel, checkpoint chunk 500: still CPU-bound in Lean when killed after 768.586s

## Possible directions

Potential fixes may include:

- Upstream-supported resumable `#prep_uplc` checkpointing.
- Memoization of normalized CEK states across checkpoint boundaries.
- Stronger caching around `runSteps` / `step` match reduction.
- Specialized reduction rules for CEK interpreter stepping.
- Better profiling or timeout diagnostics for `#prep_uplc`.

## Desired outcome

Large but nonrecursive UPLC validators should be preparable without spending minutes reducing symbolic CEK states for only a small fraction of the requested fuel budget.

Start by profiling the named CEK paths: PlutusCore.UPLC.CekMachine.runSteps, step, ifBoundOtherwiseError, and evalBuiltin, along with BuiltinFunctions.Evaluate.evaluateBuiltinFunction. Reproduce the 501-fuel measurement with checkpoint chunk 50, then determine whether checkpointing, memoization, caching, or specialized reduction is viable. Done means large nonrecursive UPLC validators prepare without multi-minute symbolic reduction.

Written by the indexing model from the issue text.