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

[spitters]

⚠️ 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 — a verified
cryptographic compiler project — currently maintains an in-tree copy of
the typed-SSA framework
(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 Rename List.getElem?_idxOf → List.getElem_idxOf (resolves name collision with Mathlib) #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 Coms 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?

[math-fehr]

Thanks for the issue.

What is the motivating use case for it? The two links you send about CatCrypt are both leading to a 404, maybe it is because the repository is private? It would help us understand what you want to do with this typed interface.

Otherwise, we have been thinking of ideas for a typed interface, but this is not something that we believe is ready to implement currently. We would like to first make sure the current untyped layer is well exercised and understood before thinking of implementing the typed layer. This is however a direction we are thinking of, but most likely in a few months rather than now. Probably understanding what your use case is would help us better plan for it!

[spitters]

I've ported part of the verified compiler https://github.com/AU-COBRA/AUCurves to Lean.
That one targets C, rust, jasmin, ...

In Lean I've targeted something close to the lean-mlir dialect. But I understand that VeIR is the new lean-mlir.
So, I'm trying to migrate. I have something that seems to work for me. I can send a PR, or I can wait for you to stabilize