IR Validation

Validation helpers for NN.IR.Graph.

There are two validation levels:

• Graph.checkWellFormed lives in NN.IR.Graph and checks only graph structure: id discipline, parent arity, and topological ordering.
• Graph.checkShapes lives here and checks the declared Node.outShapes against the shared shape inference rules from NN.IR.Infer.

Shape logic has one source of truth: Infer.inferNodeOutShape states the per-op shape rules, and Graph.checkShapes validates graph nodes through those rules.

Prop-level well-formedness wrappers

The IR layer primarily exposes executable checkers (checkWellFormed, checkShapes) because that is what compilers/backends/exporters need: either accept a graph or produce a readable error.

For proofs it is often nicer to assume a proposition instead of carrying around Except String: WellFormed g means the checker succeeds, and similarly for WellShaped g.

These wrappers keep the executable checker names and proposition-level assumptions in the same module.

def NN.IR.Graph.WellFormed (g : Graph) : Prop

Core structural well-formedness (ids, arity, topo order), as a proposition.

def NN.IR.Graph.WellShaped (g : Graph) : Prop

Shape-consistency well-formedness (WellFormed + extra shape/axis checks), as a proposition.