[Compiler]: Adding verification to the layout-algebra ops — what's the right approach?

We don't verify any of the layout ops — git grep hasVerifier include/flydsl/Dialect/Fly is empty. All 82 ops in FlyOps.td lean on TableGen operand types and InferTypeOpInterface, nothing else.

That's the wrong half to skip. In a layout DSL the algebra is the contract: composition, logical_divide, complement, right_inverse all have real preconditions — congruent shape/stride, an admissible composition, a tiler that actually divides, an invertible domain. Break one and you don't get "slightly off", you get coordinates landing on the wrong addresses, surfacing as GPU garbage several lowering stages downstream from the op that was actually wrong. Yet inferReturnTypes (lib/Dialect/Fly/IR/FlyOps.cpp) only checks type kinds: it catches "not an IntTupleType" but lets make_layout do LayoutAttr::get(shape, stride) with no congruence check, and composition/divide/inverse fall straight into the builder — silent nonsense, or an assert deep down with no location.

So the question isn't whether to verify, it's where and how much:

• Where — these ops already do the algebra in inferReturnTypes to infer their result type, so a separate verify() just redoes that same math. I'd lean toward folding the precondition checks into inferReturnTypes (already returns failure() with a Location) and keeping verify() only for ops that don't infer. Your convention call, though.
• How much — dynamic extents (IntTuple SSA values, dynamic BasisAttr leaves) mean a static check only ever sees the profile, not runtime values. So congruence/rank is checkable; value divisibility mostly isn't. Probably: enforce structure statically, defer divisibility. This overlaps #574, so I'd want it aligned with where BasisAttr is heading.

If that's the right shape, I'd factor the predicates (congruent, compatible, is_admissible_composition, …) as shared C++ next to LayoutBuilder/BasisAttr, start with make_layout + composition + logical_divide plus -verify-diagnostics tests under tests/mlir/, then fan out. Happy to take it — just want your steer on those two first.

cc @sjfeng1999 @coderfeli

Start with lib/Dialect/Fly/IR/FlyOps.cpp and include/flydsl/Dialect/Fly/FlyOps.td to trace the existing inferReturnTypes logic and operand definitions. Read the shared LayoutBuilder/BasisAttr code, then inspect tests/mlir/ for -verify-diagnostics coverage. Done means an agreed verification approach, structural checks for the initial layout operations, and tests covering their diagnostics.