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.

def NN.IR.Graph.checkShapes (g : Graph) : Except String Unit

Validate declared IR shapes using the central inference rules.

This wrapper keeps the public checker name aligned with Graph.checkInferredShapes, so callers, widgets, and backends all use the same per-op shape contracts.

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.

theorem NN.IR.Graph.wellFormed_iff (g : Graph) : g.WellFormed ↔ g.checkWellFormed = Except.ok ()

WellFormed g is just the proposition that checkWellFormed returns .ok ().

theorem NN.IR.Graph.wellShaped_iff (g : Graph) : g.WellShaped ↔ g.checkShapes = Except.ok ()

WellShaped g is just the proposition that checkShapes returns .ok ().