Roadmap question: typed-SSA layer in Veir (Com/Expr/Ctxt) — community contribution?

> ⚠️ This issue is LLM-generated based on a downstream user's notes — please flag if anything is misframed.

### Summary

Are there concrete plans to bring `opencompl/lean-mlir`'s typed-SSA layer
(the `Com` / `Expr` / `Ctxt` / `HVector` / `TyDenote` / `DialectSignature`
framework from `LeanMLIR/Framework/Basic.lean`) into Veir itself, so
downstream projects don't have to depend on both packages separately?

If yes, what's the expected timeline + design?

If a community PR adding this layer would be welcome, we'd be happy to
draft one — we've been maintaining a stripped-down fork of the typed-SSA
layer at downstream and the design has stabilised under real use.

### Why I'm asking

[CatCrypt](https://github.com/spitters/CatCrypt) — a verified
cryptographic compiler project — currently maintains an in-tree copy of
the typed-SSA framework
([`CatCrypt/Crypto/SecureCompilation/VIR/Core.lean`](https://github.com/spitters/CatCrypt/blob/master/CatCrypt/Crypto/SecureCompilation/VIR/Core.lean))
because:

* Veir doesn't yet expose typed-SSA primitives — its `IRContext` /
`OperationPtr` / `Block` model is untyped at the value level.
* Adding `opencompl/lean-mlir` as a separate dependency alongside Veir
pulls in `Veir.ForLean`'s polyfills that collide with Mathlib (see
the now-merged-or-pending PR #626 for one specific collision).
* `lean-mlir`'s current `lean-toolchain` is on `nightly-2025-12-01`,
which conflicts with downstream's Lean 4.29.1 stable pin.

A typed-SSA layer **inside Veir** would let downstream projects depend
on one upstream (Veir) for both their typed front-end and their
imperative IR back-end, with a `Com → IRContext` lowering bridging
them.

### Concrete proposal

If a community PR is welcome, a minimum-viable contribution looks like:

1. **New module**: `Veir/TypedSSA/Basic.lean` mirroring
`lean-mlir`'s `LeanMLIR/Framework/Basic.lean`:
* `Dialect`, `TyDenote`, `HVector`, `Ctxt`, `Ctxt.Var`,
`Ctxt.Valuation`, `DialectSignature`, `DialectDenote`
* `Expr d Γ ts`, `Com d Γ ts`, `Expr.denote`, `Com.denote`
* `LawfulOpDenote`, `Lets`, basic recursion utilities
2. **New lowering**: `Veir/TypedSSA/Lowering.lean` providing
`lowerCom : Com d Γ ts → IRContext O` and the typeclasses
(`ToVeirOp`, `ToVeirTy`) needed to bridge a typed dialect to
Veir's op-code enum. CatCrypt has a working version at
[`VIR/ComToVeir.lean`](...) ready to upstream.
3. **Optional**: an MLIR-text emitter for typed `Com`s using Veir's
existing `Printer.printModule`. CatCrypt has the shim at
[`VIR/VeirPrinterShim.lean`](...).

The typed-SSA module would be additive — no impact on Veir's existing
`IRContext`-based API. Downstream users who want only the imperative
graph continue to use what's there today; users wanting typed-SSA
import the new module.

### Questions

1. **Plans**: do you already have this on the roadmap? If so, what's
the planned design and timeline?
2. **Welcome a community PR?**: would you accept a contribution along
the lines above, or do you prefer to do this in-house?
3. **Design preferences**: if a PR would be welcome:
* Verbatim port of `lean-mlir`'s typed-SSA, or a leaner version
tailored for Veir's use cases?
* Module path — `Veir/TypedSSA/*` or somewhere else?
* Naming conventions — keep `Com`/`Expr`/`Ctxt` or rename?
* Effect annotations (`EffectKind` from `lean-mlir`) — include or
omit?