Optimizer emits kernel-ill-typed Blaster.dite'; test harness never typechecks, so expectations encode the bad terms

## Summary

The optimizer can produce `Blaster.dite'` terms that the Lean **kernel rejects**. The test suite does not notice, because it compares optimizer output *structurally* and never typechecks it. As a result several expected outputs currently committed in `Tests/` are themselves ill-typed terms.

This is not a theoretical concern: it is a hard stop for `#prep_uplc`, which turns the optimized term into a declaration via `addDecl` and therefore *does* invoke the kernel. On the CIP-113 "programmable tokens" validators this kills the prep outright with an `application type mismatch` naming `Blaster.dite'`.

We hit this while formalizing those validators, wrote a fix, and have been carrying it on a fork. We would much rather not maintain a fork — hence this report. Everything below is reproducible with nothing but this repo.

## Why the term is ill typed

`Blaster.dite'` is well typed only when the two branch binder types are **syntactically** `c` and `¬c` for the condition `c`:

```lean
Blaster.dite' c (fun _ : c => …) (fun _ : ¬c => …)
```

But the condition and the branch binder types travel through the optimizer **independently**:

- the condition is optimized on its own — `Blaster/Optimize/Basic.lean:111`, pushing `.DiteChoiceWaitForCond`;
- each branch lambda's binder **type** is optimized separately — `optimizeDiteArg` at `Blaster/Optimize/Basic.lean:229` → `optimizeLambda`;
- the `inDite` flag in `Blaster/Optimize/OptimizeStack.lean:259-268` only feeds `addHypotheses`; it does not re-type the binders;
- the pieces are reassembled with no consistency check — `Blaster/Optimize/Rewriting/OptimizeITE.lean:423`:

```lean
mkApp4Expr f iteType c t e
```

So whenever `optimize(¬c)` is not syntactically `¬ optimize(c)`, the rebuilt `dite'` is ill typed. Two normalisations in `Blaster/Optimize/Rewriting/OptimizePropNot.lean` do exactly that:

| normalisation | condition stays | branch binder becomes |
|---|---|---|
| `¬(true = e)` → `false = e` (`OptimizePropNot.lean:15-18, 27-28`) | `true = e` | `false = e` |
| `¬(¬a ∧ ¬b)` → `a ∨ b` (De Morgan) | `¬a ∧ ¬b` | `a ∨ b` |

## Reproduction (self-contained, no external deps)

The optimizer entry point is the same one `#testOptimize` uses; the only thing added is the kernel check that `#testOptimize` never performs.

```lean
import Lean
import Blaster

open Lean Elab Command Term Meta

syntax (name := kcheck) "#kernelCheck" str term : command

@[command_elab kcheck]
def kcheckImpl : CommandElab := fun stx => do
match stx with
| `(#kernelCheck $nm:str $t:term) => do
liftTermElabM do
withTheReader Core.Context (fun ctx => { ctx with maxHeartbeats := 0 }) do
let e ← elabTermAndSynthesize t none
let (opt, _) ← Blaster.Optimize.command ({} : Blaster.Options.BlasterOptions) e
let declName := Name.mkSimple ("d6_kernel_check_" ++ nm.getString)
try
addDecl (.defnDecl {
name := declName, levelParams := [], type := mkSort levelZero,
value := opt, hints := .abbrev, safety := .safe })
logInfo m!"{nm.getString} ✅ KERNEL ACCEPTED"
catch ex =>
logError m!"{nm.getString} ❌ KERNEL REJECTED :: {ex.toMessageData}"
| _ => throwUnsupportedSyntax

-- Verbatim input of your own test DIteCondUnchanged_3
-- (Tests/Optimize/OptimizeITE/OptimizeDITE.lean:670-672)
#kernelCheck "DIteCondUnchanged_3"
∀ (a b : Bool) (x y z : Nat) (f : b && (a || !a) → Nat → Nat),
(if h : b && (a || !a) then (f h x + 40) - 40 else y) < z

-- Verbatim input of your own test BoolEqDIteUnchanged_1
-- (Tests/Optimize/OptimizeDecide/DecideEq.lean:1255)
#kernelCheck "DeMorganCond"
∀ (p q : Prop) (x y z : Nat) [Decidable p] [Decidable q] (f : ¬ p ∧ ¬ q → Nat → Nat),
(if h : ¬ p ∧ ¬ q then f h x else y) < z
```

On `beta-lambda-cache-optimization` @ `59db213`:

```
error: (kernel) application type mismatch
Blaster.dite' (true = b) (fun h => f h x) fun h => y
argument has type false = b → Nat
but function has type (¬true = b → Nat) → Nat
```

and likewise for the De Morgan case: `p ∨ q → Nat` where `¬(¬p ∧ ¬q) → Nat` was required.

Note both inputs are **your own test cases, unmodified**. They pass `#testOptimize` today.

## Why the suite doesn't catch it

`Tests/Utils.lean:172` is the whole check:

```lean
if actual == expected
then logInfo f!"{name} ✅ Success!"
else logError f!"{name} ❌ Failure! …"
```

This is structural `BEq` on `Expr`, inside `withoutModifyingEnv` — no `addDecl`, no `inferType`, no kernel involvement. An ill-typed term compares equal to an ill-typed expectation and the test goes green.

Consequently some committed expectations encode ill-typed terms. `Tests/Optimize/OptimizeITE/OptimizeDITE.lean:599-666` (`diteCondUnchanged_3`) is the clearest: its `dite'` has condition `Eq Bool Bool.true (bvar 4)` (`true = b`), then-binder `Eq Bool Bool.true (bvar 4)` — correct — and **else-binder `Eq Bool Bool.false (bvar 4)`**, i.e. `false = b` where `¬(true = b)` is required.

## Scale

Instrumenting the harness to typecheck every optimizer output across `OptimizeDITE`, `OptimizeITE` and `OptimizeDecide.DecideEq`:

| | kernel-invalid | kernel-valid |
|---|---:|---:|
| `59db213` as-is | **36** | 578 |
| with the fix below | **9** | 605 |

The remaining 9 are branches whose body actually *uses* its proof binder; the fix deliberately declines those (see below).

## The fix we've been carrying

One function plus one call site in `Blaster/Optimize/Rewriting/OptimizeITE.lean` — rebuild the branch binder types from the **final** optimized condition (`c` for then, `Not c` for else) at the reassembly point.

Soundness argument: `dite'` ignores the `Decidable` instance and its branches take a computationally irrelevant proof argument. When a branch lambda does not use its proof binder (`!body.hasLooseBVars` — true of every branch the optimizer builds by normalisation) the binder's type is unconstrained by the body, so it can be restated as whatever `dite'` requires. When the body *does* use the binder, nothing is changed:

```lean
if body.hasLooseBVars || exprEq bty ty then return b
```

So the transformation can only repair a term the kernel would have rejected. It never alters an accepted term and never touches a branch body.

Branch, rebased onto your `beta-lambda-cache-optimization` tip and building clean:
**https://github.com/Anastasia-Labs/Lean-blaster/tree/d6-on-beta-lambda-cache** (single commit `4d320dd` on top of `59db213`).

## What adopting it costs

27 tests go red — **all of them expectation conflicts, not behavioural regressions**. Those 27 are a strict subset of the 36 cases where `59db213` already emits kernel-invalid terms, so the fix repairs 27 and breaks 0 legitimate cases. Adopting it means regenerating those 27 expectations.

## Suggestions

1. **Typecheck in the harness.** Adding a kernel check (or at least `inferType`) to `Tests/Utils.lean:172` would have caught this and would prevent ill-typed expectations from being committed in future. We think this is the higher-value change — the `dite'` fix addresses one symptom, the blind spot is the cause.
2. Take the fix (or an equivalent), and regenerate the 27 affected expectations.

Happy to open a PR for either, adjust the approach, or hand over more detail — just say which you'd prefer. Related: #138 (`#prep_uplc` scaling), which we hit on the same validators.

Start with Blaster/Optimize/Rewriting/OptimizeITE.lean:423, then read the condition and branch handling in Blaster/Optimize/Basic.lean, Blaster/Optimize/OptimizeStack.lean, and Blaster/Optimize/Rewriting/OptimizePropNot.lean. Run the supplied kernel-check reproductions and inspect Tests/Utils.lean:172 plus the affected optimizer tests; done means invalid optimized terms are rejected by the harness and the affected expectations are regenerated without legitimate regressions.

Written by the indexing model from the issue text.