[performance] Hash-consing revisits noncanonical shared DAGs exponentially

## Summary

Hash-consing a physically shared expression graph can take exponential work when canonicalization changes child pointers. The intern table stores canonical nodes but does not retain an original-node-to-canonical-node mapping for the current walk.

**An existing fix is already present in PR #160**, in `Blaster/Optimize/Env/HashConsing.lean` at `Anastasia-Labs/Lean-blaster@9caca28412f96415487f743417a8d1d7a00e8f50`. This focused issue supplies a minimal typed regression and tracks bringing that fix onto the current optimization stack. It is related to #138, but requires no CEK code, garbage collection, cache eviction, or large input file to reproduce. This is a performance issue; no incorrect logical result has been demonstrated.

## Reproducer

Save the following as `Tests/Benchmarks/HashConsDAGRepro.lean` and run `lake build Tests.Benchmarks.HashConsDAGRepro`. The two lambda binder names deliberately canonicalize to the same identity function. Each layer references the preceding expression twice, so the allocated input graph grows linearly with depth.

```lean
import Tests.Utils
import Blaster.Optimize.Env.HashConsing

open Lean Meta Elab Command Blaster.Optimize
namespace HashConsDAGRepro
set_option maxHeartbeats 0

/-- A linear-sized, physically shared, well-typed Nat expression. The first
identity seeds the canonical binder name; the shared graph uses another name. -/
def input (depth : Nat) : Expr := Id.run do
let nat := mkConst ``Nat
let zero := mkNatLit 0
let canonical := mkApp (.lam `canonical nat (.bvar 0) .default) zero
let mut shared := mkApp (.lam `renamed nat (.bvar 0) .default) zero
for _ in [:depth] do
shared := mkApp2 (mkConst ``Nat.add) shared shared
return mkApp2 (mkConst ``Nat.add) canonical shared

run_cmd liftTermElabM do
for depth in #[8, 12, 16, 20] do
let measure : TranslateEnvT Unit := do
let e := input depth
let started ← IO.monoMsNow
let beats ← IO.getNumHeartbeats
let result ← hashcons e
let allocated := (← IO.getNumHeartbeats) - beats
let elapsed := (← IO.monoMsNow) - started
let count := (← get).optEnv.hashConsCache.size
unless (← inferType result).isConstOf ``Nat do throwError "wrong result type"
logInfo m!"HASHCONS_DAG depth={depth} ms={elapsed} allocations={allocated} entries={count}"
measure.run' (default : TranslateEnv)

elab "hashcons_diamond " n:num : term => pure (input n.getNat)

#testOptimize ["HashConsDAGOptimize"] (norm-result: 1)
(hashcons_diamond 16) ===> (0 : Nat)

end HashConsDAGRepro
```

## Observed

On Lean 4.24.0 / Apple M2 Max, with the walker unchanged from the current PR #248 head `2cc060ca2739f4270490530924425a395769bd2e`:

| Depth | Hash-cons time | Raw allocation-heartbeat delta | Final intern entries |
| --- | ---: | ---: | ---: |
| 8 | <1 ms | 10,226 | 90 |
| 12 | 3 ms | 155,845 | 98 |
| 16 | 51 ms | 2,490,609 | 106 |
| 20 | 831 ms | 39,846,173 | 114 |

Times are single diagnostic measurements. The roughly 16-fold work increase per four layers, despite only eight additional intern entries, exposes the repeated traversal. `#testOptimize` still produces the correct result.

This was found while interning kernel-certified CEK block expressions: a Governance scout timed out at 180 seconds, and every active sample in a separate diagnostic window was inside `hashcons`. The minimal reproduction above isolates the walker independently of that experimental compiler.

## Expected

Traversal should scale with the number of distinct input nodes and edges, even when canonical children differ from their original pointers. Preserve the existing canonicalization/binder behavior and avoid retaining a source-node memo beyond the current walk.

The narrow port should credit/reuse PR #160, add an `Issue.lean` regression with a Blaster/`#testOptimize` check and a generous allocation-work bound, and validate ordinary Cardano preparation as well as the staging workload. The broader GC/retention changes in #160 are outside this fix.

Start with the reproducer in Tests/Benchmarks/HashConsDAGRepro.lean and the hashcons entry point in Blaster/Optimize/Env/HashConsing.lean; run lake build Tests.Benchmarks.HashConsDAGRepro and compare the current walker with the existing fix in PR #160. Done means adding the focused Issue.lean regression and #testOptimize check, bounding allocation work, and validating Cardano preparation and the staging workload.

Written by the indexing model from the issue text.