IR Node Lowering

The exhaustive checked compiler loop from operation-tagged IR nodes to executable SSA nodes.

@[irreducible]

def Runtime.Autograd.Compiled.IRExec.buildFrom {α : Type} [Context α] [DecidableEq Spec.Shape] (g : NN.IR.Graph) (payload : NN.IR.Payload α) (inShape : Spec.Shape) (i : ℕ) (st : State α inShape) : Except String (State α inShape)

Compile the IR graph starting at node index i, extending the current SSA State.

This is the main compiler loop:

• it checks i < g.nodes.size,
• compiles node i into a NodeData.forward closure (rejecting unsupported ops/shapes), and
• snocs the resulting node into the accumulating GraphData.

The public entrypoint execGraphOfIR handles node 0 and calls buildFrom starting at i = 1.

Operationally, buildFrom is a checked compiler:

• success means every visited node had well-typed parents and a supported lowering case,
• failure returns a concrete error explaining the first unsupported/malformed node.